feat(hott/homotopy): continue defining squares for join associativity

hott/cubical/cube.hlean

@@ -157,7 +157,7 @@ namespace eq
   section cube_fillers
   variables (s₁₁₀ s₁₁₂ s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁)
 
-  definition cube_fil110 : Σ lid, cube lid s₁₁₂ s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ :=
+  definition cube_fill110 : Σ lid, cube lid s₁₁₂ s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ :=
   begin
     induction s₀₁₁, induction s₂₁₁,
     let fillsq := square_fill_l (eq_of_vdeg_square s₁₀₁) 

hott/cubical/square.hlean

@@ -76,14 +76,14 @@ namespace eq
     square p₁₀ p₁₂ p₀₁ p :=
   by induction r; exact s₁₁
 
-  infix ` ⬝h `:75 := hconcat
-  infix ` ⬝v `:75 := vconcat
-  infix ` ⬝hp `:75 := hconcat_eq
-  infix ` ⬝vp `:75 := vconcat_eq
-  infix ` ⬝ph `:75 := eq_hconcat
-  infix ` ⬝pv `:75 := eq_vconcat
-  postfix `⁻¹ʰ`:(max+1) := hinverse
-  postfix `⁻¹ᵛ`:(max+1) := vinverse
+  infix `⬝h`:75 := hconcat --type using \tr
+  infix `⬝v`:75 := vconcat --type using \tr
+  infix `⬝hp`:75 := hconcat_eq --type using \tr
+  infix `⬝vp`:75 := vconcat_eq --type using \tr
+  infix `⬝ph`:75 := eq_hconcat --type using \tr
+  infix `⬝pv`:75 := eq_vconcat --type using \tr
+  postfix `⁻¹ʰ`:(max+1) := hinverse --type using \-1h
+  postfix `⁻¹ᵛ`:(max+1) := vinverse --type using \-1v
 
   definition transpose [unfold 10] (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) : square p₀₁ p₂₁ p₁₀ p₁₂ :=
   by induction s₁₁;exact ids
@@ -499,4 +499,9 @@ namespace eq
   definition square_fill_r : Σ (p : a₂₀ = a₂₂) , square p₁₀ p₁₂ p₀₁ p :=
   by induction p₁₀; induction p₁₂; exact ⟨_, !hrefl⟩
 
+  --TODO find better names
+  definition square_Fl_Fl_ap_idp {A B : Type} {b : B} {f : A → B} (p : Π a, f a = b)
+    {a₀ a₁ : A} (q : a₀ = a₁) : square (p a₀) (p a₁) (ap f q) idp  :=
+  by induction q; apply vrfl
+
 end eq

hott/homotopy/join.hlean

@@ -6,17 +6,19 @@ Authors: Jakob von Raumer
 Declaration of a join as a special case of a pushout
 -/
 
-import hit.pushout .susp
+import hit.pushout .susp cubical.cube cubical.squareover
 
-open eq function prod equiv pushout is_trunc bool
+open eq function prod equiv pushout is_trunc bool sigma.ops function
 
 namespace join
+  section
+  variables (A B C : Type)
 
-  definition join (A B : Type) : Type := @pushout (A × B) A B pr1 pr2
+  definition join : Type := @pushout (A × B) A B pr1 pr2
 
   definition jglue {A B : Type} (a : A) (b : B) := @glue (A × B) A B pr1 pr2 (a, b)
 
-  protected definition is_contr (A B : Type) [HA : is_contr A] :
+  protected definition is_contr [HA : is_contr A] :
     is_contr (join A B) :=
   begin
     fapply is_contr.mk, exact inl (center A),
@@ -26,7 +28,7 @@ namespace join
     generalize center_eq a, intro p, cases p, apply idp_con,
   end
 
-  protected definition bool (A : Type) : join bool A ≃ susp A :=
+  protected definition bool : join bool A ≃ susp A :=
   begin
     fapply equiv.MK, intro ba, induction ba with b a,
       induction b, exact susp.south, exact susp.north, exact susp.north,
@@ -60,14 +62,13 @@ namespace join
       apply square_of_eq_top, rewrite idp_con, apply !con.right_inv⁻¹,   
   end
 
-  protected definition swap (A B : Type) :
-    join A B → join B A :=
+  protected definition swap : join A B → join B A :=
   begin
     intro x, induction x with a b, exact inr a, exact inl b,
     apply !jglue⁻¹
   end
 
-  protected definition swap_involutive (A B : Type) (x : join A B) :
+  protected definition swap_involutive (x : join A B) :
     join.swap B A (join.swap A B x) = x :=
   begin
     induction x with a b, do 2 reflexivity,
@@ -78,30 +79,70 @@ namespace join
     krewrite [elim_glue, ap_inv, elim_glue], apply inv_inv,
   end
 
-  protected definition symm (A B : Type) : join A B ≃ join B A :=
+  protected definition symm : join A B ≃ join B A :=
   begin
     fapply equiv.MK, do 2 apply join.swap,
     do 2 apply join.swap_involutive,
   end
 
-  protected definition switch (A B C : Type) :
-    join (join A B) C → join (join C B) A :=
-  begin
-    intro x, induction x with ab c,
-    induction ab with a b, exact inr a, exact inl (inr b),
-    apply !jglue⁻¹, exact inl (inl c), esimp,
-    induction x with ab c, induction ab with a b, apply !jglue⁻¹,
-    apply ap inl, apply !jglue⁻¹, induction x with a b, esimp,
-    let H := eq_of_square (square_of_pathover (apdo (λ x, jglue x a) (jglue c b))),
-    rewrite [ap_constant at H, con_idp at H], apply eq_pathover, esimp,
-    krewrite [elim_glue, ap_constant, ap_inv], esimp, apply hinverse,
-    esimp at *, apply square_of_eq, krewrite [H, con.assoc, con.right_inv],
-    krewrite [idp_con],
   end
-  print definition join.switch
 
-  protected definition switch_involutive (A B C : Type) (x : join (join A B) C) :
-    join.switch C B A (join.switch A B C x) = x := sorry
+  --This proves that the join operator is associative
+  --The proof is more or less ported from Evan Cavallo's agda version
+  section switch_assoc
+  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 :=
+  by induction sq; exact ids
+
+  variables {A B C : Type}
+
+  private definition switch_left : join A B → join (join C B) A :=
+  begin
+    intro x, induction x with a b, exact inr a, exact inl (inr b), apply !jglue⁻¹,
+  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,
+      cube hrfl hrfl (hdeg_square !elim_glue) ids 
+        sq (eq_hconcat !idp_con⁻¹ (massage_sq (square_Fl_Fl_ap_idp _ _))) :=
+  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 (switch_coh_fill _ _ _).1,
+  end
+
+  protected definition switch : join (join A B) C → join (join C B) A :=
+  begin
+    intro x, induction x with ab c, exact switch_left ab, exact inl (inl c),
+    induction x with ab c, exact switch_coh ab c,
+  end
+
+  private definition switch_inv_left_square (a : A) (b : B) :
+    square idp idp (ap (!(@join.switch C) ∘ switch_left) (jglue a b)) (ap inl (jglue a b)) :=
+  begin
+    refine hdeg_square !ap_compose ⬝h _,
+    refine aps join.switch (hdeg_square !elim_glue) ⬝h _, esimp,
+    refine hdeg_square !(ap_inv join.switch) ⬝h _,
+    refine hrfl⁻¹ʰ⁻¹ᵛ ⬝h _, esimp[join.switch,switch_left,switch_coh],
+    refine (hdeg_square !elim_glue)⁻¹ᵛ ⬝h _, esimp,
+    refine (hdeg_square !ap_inv)⁻¹ᵛ ⬝h _, apply hdeg_square !inv_inv,
+  end
+
+  private definition switch_inv_coh_left (c : C) (a : A) :
+    square idp idp (ap !(@join.switch C B) (switch_coh (inl a) c)) (jglue (inl a) c) :=
+  begin
+    refine hrfl ⬝h _,
+    refine 
+  end
+
+
+  end switch_assoc
+
+exit
 
   protected definition switch_equiv (A B C : Type) :
     join (join A B) C ≃ join (join C B) A :=