feat(hott/homotopy): progress on join associativity, many coherence lemmas about square operations needed

hott/cubical/cube.hlean

@@ -176,11 +176,11 @@ namespace eq
     (hdeg_square s₂₁) (hdeg_square s₁₀) (hdeg_square s₁₂) ids ids :=
   by induction p₀₀; induction sq; apply idc
 
-  definition ids2_cube_of_square : cube ids ids
+  definition ids1_cube_of_square : cube ids ids
     (vdeg_square s₁₀) (vdeg_square s₁₂) (hdeg_square s₀₁) (hdeg_square s₂₁) :=
   by induction p₀₀; induction sq; apply idc
 
-  definition ids1_cube_of_square : cube (vdeg_square s₁₀) (vdeg_square s₁₂)
+  definition ids2_cube_of_square : cube (vdeg_square s₁₀) (vdeg_square s₁₂)
     ids ids (vdeg_square s₀₁) (vdeg_square s₂₁) :=
   by induction p₀₀; induction sq; apply idc
 
@@ -200,7 +200,7 @@ namespace eq
     apply cube_transport101 (left_inv (vdeg_square_equiv _ _) s₁₀₁),
     apply cube_transport112 (left_inv (hdeg_square_equiv _ _) s₁₁₂),
     apply cube_transport121 (left_inv (vdeg_square_equiv _ _) s₁₂₁),
-    apply ids2_cube_of_square, exact fillsq.2
+    apply ids1_cube_of_square, exact fillsq.2
   end
 
   definition cube_fill112 : Σ lid, cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀ lid :=
@@ -212,7 +212,7 @@ namespace eq
     apply cube_transport101 (left_inv (vdeg_square_equiv _ _) s₁₀₁),
     apply cube_transport110 (left_inv (hdeg_square_equiv _ _) s₁₁₀),
     apply cube_transport121 (left_inv (vdeg_square_equiv _ _) s₁₂₁),
-    apply ids2_cube_of_square, exact fillsq.2,
+    apply ids1_cube_of_square, exact fillsq.2,
   end
 
   definition cube_fill011 : Σ lid, cube lid s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂ :=
@@ -224,7 +224,7 @@ namespace eq
     apply cube_transport110 (left_inv (vdeg_square_equiv _ _) s₁₁₀),
     apply cube_transport211 (left_inv (vdeg_square_equiv _ _) s₂₁₁),
     apply cube_transport112 (left_inv (vdeg_square_equiv _ _) s₁₁₂),
-    apply ids1_cube_of_square, exact fillsq.2,
+    apply ids2_cube_of_square, exact fillsq.2,
   end
 
   definition cube_fill211 : Σ lid, cube s₀₁₁ lid s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂ :=
@@ -236,7 +236,7 @@ namespace eq
     apply cube_transport011 (left_inv (vdeg_square_equiv _ _) s₀₁₁),
     apply cube_transport110 (left_inv (vdeg_square_equiv _ _) s₁₁₀),
     apply cube_transport112 (left_inv (vdeg_square_equiv _ _) s₁₁₂),
-    apply ids1_cube_of_square, exact fillsq.2,
+    apply ids2_cube_of_square, exact fillsq.2,
   end
 
   definition cube_fill101 : Σ lid, cube s₀₁₁ s₂₁₁ lid s₁₂₁ s₁₁₀ s₁₁₂ :=
@@ -265,4 +265,10 @@ namespace eq
 
   end cube_fillers
 
+  include c
+  definition apc (f : A → B) :
+    cube (aps f s₀₁₁) (aps f s₂₁₁) (aps f s₁₀₁) (aps f s₁₂₁) (aps f s₁₁₀) (aps f s₁₁₂) :=
+  by cases c; exact idc
+  omit c
+
 end eq

hott/cubical/square.hlean

@@ -500,10 +500,14 @@ namespace eq
   by induction p₁₀; induction p₁₂; exact ⟨_, !hrefl⟩
 
   --TODO find better names
-  definition square_Flr_ap_idp {A B : Type} {b : B} {f : A → B} (p : Π a, f a = b)
+  definition square_Flr_ap_idp {A B : Type} {c : B} {f : A → B} (p : Π a, f a = c)
     {a b : A} (q : a = b) : square (p a) (p b) (ap f q) idp  :=
   by induction q; apply vrfl
 
+  definition square_Flr_idp_ap {A B : Type} {c : B} {f : A → B} (p : Π a, c = f a)
+    {a b : A} (q : a = b) : square (p a) (p b) idp (ap f q) :=
+  by induction q; apply vrfl
+
   definition square_ap_idp_Flr {A B : Type} {b : B} {f : A → B} (p : Π a, f a = b)
     {a b : A} (q : a = b) : square (ap f q) idp (p a) (p b) :=
   by induction q; apply hrfl

hott/homotopy/join.hlean

@@ -89,7 +89,7 @@ namespace join
 
   --This proves that the join operator is associative
   --The proof is more or less ported from Evan Cavallo's agda version
-  section switch_assoc
+  section join_switch
   private definition massage_sq {A : Type} {a₀₀ a₂₀ a₀₂ a₂₂ : A}
     {p₁₀ : a₀₀ = a₂₀} {p₁₂ :  a₀₂ = a₂₂} {p₀₁ : a₀₀ = a₀₂} {p₂₁ : a₂₀ = a₂₂}
     (sq : square p₁₀ p₁₂ p₀₁ p₂₁) : square p₁₀⁻¹ p₀₁⁻¹ (p₂₁ ⬝ p₁₂⁻¹) idp :=
@@ -103,15 +103,15 @@ namespace join
   end
 
   private definition switch_coh_fill (a : A) (b : B) (c : C) :
-    Σ sq : square (jglue (inl c) a)⁻¹ (ap inl (jglue c b))⁻¹ (ap switch_left (jglue a b)) idp,
+    Σ sq : square (jglue (inl c) a)⁻¹ (ap inl (jglue c b)⁻¹) (ap switch_left (jglue a b)) idp,
-      cube hrfl hrfl (hdeg_square !elim_glue) ids 
+      cube (hdeg_square !elim_glue) ids sq
-        sq (eq_hconcat !idp_con⁻¹ (massage_sq (square_Fl_Fl_ap_idp _ _))) :=
+        (!idp_con⁻¹ ⬝ph (massage_sq (square_Flr_ap_idp _ _)) ⬝vp !ap_inv⁻¹) hrfl hrfl :=
   by esimp; apply cube_fill101
 
   private definition switch_coh (ab : join A B) (c : C) : switch_left ab = inl (inl c) :=
   begin
     induction ab with a b, apply !jglue⁻¹, apply ap inl !jglue⁻¹, induction x with a b,
-    apply eq_pathover, refine _ ⬝hp !ap_constant⁻¹, refine _ ⬝vp !ap_inv⁻¹,
+    apply eq_pathover, refine _ ⬝hp !ap_constant⁻¹,
     apply !switch_coh_fill.1,
   end
 
@@ -164,19 +164,37 @@ namespace join
 
   section
   variables (a : A) (b : B) (c : C)
-  check cube ids (switch_inv_left_square a b)
 
-  private definition switch_inv_cube (a : A) (b : B) (c : C) :
+  private definition switch_inv_cube_aux1 {A B C : Type} {b : B} {f : A → B} (h : B → C)
-    cube ids (switch_inv_left_square a b)
+    (g : Π a, f a = b) {x y : A} (p : x = y) :
-      (square_Fl_Fl_ap_idp _ _) (square_Fl_Fl_ap_idp _ _)
+    cube (hdeg_square (ap_compose h f p)) ids (square_Flr_ap_idp (λ a, ap h (g a)) p)
-      --(switch_inv_coh_left c a) (switch_inv_coh_right c b)
+    (aps h (square_Flr_ap_idp _ _)) hrfl hrfl :=
-      :=
   begin
-
+    cases p, esimp[square_Flr_ap_idp], apply deg2_cube,
+    cases (g x), reflexivity,
   end
 
+  private definition switch_inv_cube_aux2 {A B C : Type} {b : B} {f : A → B}
+    (g : Π a, f a = b) {x y : A} (p : x = y) {sq : square (g x) (g y) (ap f p) idp}
+    (q : apdo g p = eq_pathover (sq ⬝hp !ap_constant⁻¹)) : square_Flr_ap_idp _ _ = sq :=
+  begin
+    cases p, esimp at *, exact sorry
+  end
 
-  end switch_assoc
+  private definition switch_inv_cube (a : A) (b : B) (c : C) :
+    cube (switch_inv_left_square a b) ids (square_Flr_ap_idp _ _)
+    (square_Flr_ap_idp _ _) (switch_inv_coh_left c a) (switch_inv_coh_right c b) :=
+  begin
+    esimp [switch_inv_coh_left, switch_inv_coh_right, switch_inv_left_square],
+    apply cube_concat2, apply switch_inv_cube_aux1,
+    apply cube_concat2, esimp, apply cube_transport101,
+      apply inverse, apply ap (λ x, aps join.switch x),
+      apply switch_inv_cube_aux2, esimp[switch_coh, jglue], apply rec_glue,
+      apply apc, apply (switch_coh_fill a b c).2,
+  end
+  check ap_constant
+
+  end join_switch 
 
 exit