From e481e541a2a0cc53fea97ff33616764492095599 Mon Sep 17 00:00:00 2001
From: Jakob von Raumer <javra@web.de>
Date: Tue, 24 Nov 2015 17:58:53 +0000
Subject: [PATCH] feat(hott/homotopy): more progress on join associativity

---
 hott/cubical/cube.hlean  |  4 +--
 hott/homotopy/join.hlean | 68 +++++++++++++++++++++++++++++++++++++---
 2 files changed, 65 insertions(+), 7 deletions(-)

diff --git a/hott/cubical/cube.hlean b/hott/cubical/cube.hlean
index ffd370af9..1e4d4a1fc 100644
--- a/hott/cubical/cube.hlean
+++ b/hott/cubical/cube.hlean
@@ -102,7 +102,7 @@ namespace eq
       whisker_square (eq_bot_of_square s₀₁₁) (eq_bot_of_square s₂₁₁) idp idp s₁₁₂ :=
   by induction c; reflexivity
 
-  definition eq_of_vdeg_cube {s s' : square p₀₁₀ p₂₁₀ p₁₀₀ p₁₂₀}
+  definition eq_of_deg12_cube {s s' : square p₀₁₀ p₂₁₀ p₁₀₀ p₁₂₀}
     (c : cube vrfl vrfl vrfl vrfl s s') : s = s' :=
   by induction s; exact eq_of_cube c
 
@@ -113,7 +113,7 @@ namespace eq
     {r : square (f₁ a') (f₂ a') (f₃ a') (f₄ a')}
     (s : cube (vdeg_square (ap f₁ p)) (vdeg_square (ap f₂ p))
               (vdeg_square (ap f₃ p)) (vdeg_square (ap f₄ p)) q r) : q =[p] r :=
-  by induction p;apply pathover_idp_of_eq;exact eq_of_vdeg_cube s
+  by induction p;apply pathover_idp_of_eq;exact eq_of_deg12_cube s
 
   /- Transporting along a square -/
 
diff --git a/hott/homotopy/join.hlean b/hott/homotopy/join.hlean
index 1d64d846e..0d7bbba2f 100644
--- a/hott/homotopy/join.hlean
+++ b/hott/homotopy/join.hlean
@@ -187,17 +187,75 @@ namespace join
   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 cube_concat2, 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 switch_inv_cube_aux2, apply rec_glue,
       apply apc, apply (switch_coh_fill a b c).2,
+    apply cube_concat2, esimp, 
+  end
+
+  end
+
+  private definition pathover_of_triangle_cube {A B : Type} {b₀ b₁ : A → B}
+    {b : B} {p₀₁ : Π a, b₀ a = b₁ a} {p₀ : Π a, b₀ a = b} {p₁ : Π a, b₁ a = b}
+    {x y : A} {q : x = y} {sqx : square (p₀₁ x) idp (p₀ x) (p₁ x)}
+    {sqy : square (p₀₁ y) idp (p₀ y) (p₁ y)}
+    (c : cube (natural_square_tr _ _) ids (square_Flr_ap_idp p₀ q) (square_Flr_ap_idp p₁ q)
+       sqx sqy) :
+    sqx =[q] sqy :=
+  begin
+    cases q, esimp [square_Flr_ap_idp] at *,
+    apply pathover_of_eq_tr, esimp, apply eq_of_deg12_cube, exact c,
+  end
+
+  private definition pathover_of_ap_ap_square {A : Type} {x y : A} {p : x = y}
+    (g : B → A) (f : A → B) {u : g (f x) = x} {v : g (f y) = y}
+    (sq : square (ap g (ap f p)) p u v) : u =[p] v :=
+  by cases p; apply eq_pathover; apply transpose; exact sq
+
+
+  private definition hdeg_square_idp {A : Type} {a a' : A} {p : a = a'} :
+    hdeg_square (refl p) = hrfl :=
+  by cases p; reflexivity
+
+  private definition vdeg_square_idp {A : Type} {a a' : A} {p : a = a'} :
+    vdeg_square (refl p) = vrfl :=
+  by cases p; reflexivity
+
+  private definition natural_square_tr_beta {A B : Type} {f₁ f₂ : A → B}
+    (p : Π a, f₁ a = f₂ a) {x y : A} (q : x = y) {sq : square (p x) (p y) (ap f₁ q) (ap f₂ q)}
+    (e : apdo p q = eq_pathover sq) :
+    natural_square_tr p q = sq :=
+  begin
+    cases q, esimp at *,
+    apply concat, apply inverse, apply vdeg_square_idp,
+    assert H : refl (p y) = eq_of_vdeg_square sq,
+    { exact sorry },
+    apply concat, apply ap vdeg_square, exact H,
+    apply is_equiv.left_inv (equiv.to_fun !vdeg_square_equiv),
+  end
+
+  private definition switch_inv_coh (c : C) (k : join A B) :
+    square (switch_inv_left k) idp (ap join.switch (switch_coh k c)) (jglue k c) :=
+  begin
+    induction k, apply switch_inv_coh_left, apply switch_inv_coh_right,
+    refine pathover_of_triangle_cube _,
+    induction x with [a, b], esimp, apply cube_transport011,
+    apply inverse, rotate 1, apply switch_inv_cube,
+    apply natural_square_tr_beta, apply rec_glue,
+  end
+
+  protected definition switch_involutive (x : join (join A B) C) :
+    join.switch (join.switch x) = x :=
+  begin
+    induction x, apply switch_inv_left, reflexivity,
+    apply pathover_of_ap_ap_square join.switch join.switch,
+    induction x with [k, c], krewrite elim_glue, esimp,
+    apply transpose, exact !switch_inv_coh,
   end
-  check ap_constant
 
   end join_switch 
 
-exit
-
   protected definition switch_equiv (A B C : Type) :
     join (join A B) C ≃ join (join C B) A :=
   by apply equiv.MK; do 2 apply join.switch_involutive