From 54b1d1a9fe179586148d9b220226b505a6827eae Mon Sep 17 00:00:00 2001
From: Jakob von Raumer <javra@web.de>
Date: Fri, 30 Oct 2015 16:54:24 +0000
Subject: [PATCH] feat(hott/homotopy): more steps towards join associativity,
 cube composition

---
 hott/cubical/cube.hlean   | 25 +++++++++++++++++++---
 hott/cubical/square.hlean |  8 +++++--
 hott/homotopy/join.hlean  | 44 +++++++++++++++++++++++++++++++++++----
 3 files changed, 68 insertions(+), 9 deletions(-)

diff --git a/hott/cubical/cube.hlean b/hott/cubical/cube.hlean
index 3080f710c..bc168338d 100644
--- a/hott/cubical/cube.hlean
+++ b/hott/cubical/cube.hlean
@@ -12,8 +12,7 @@ open equiv equiv.ops is_equiv sigma sigma.ops
 
 namespace eq
 
-  inductive cube {A : Type} {a₀₀₀ : A}
-    : Π{a₂₀₀ a₀₂₀ a₂₂₀ a₀₀₂ a₂₀₂ a₀₂₂ a₂₂₂ : A}
+  inductive cube {A : Type} {a₀₀₀ : A} : Π{a₂₀₀ a₀₂₀ a₂₂₀ a₀₀₂ a₂₀₂ a₀₂₂ a₂₂₂ : A}
        {p₁₀₀ : a₀₀₀ = a₂₀₀} {p₀₁₀ : a₀₀₀ = a₀₂₀} {p₀₀₁ : a₀₀₀ = a₀₀₂}
        {p₁₂₀ : a₀₂₀ = a₂₂₀} {p₂₁₀ : a₂₀₀ = a₂₂₀} {p₂₀₁ : a₂₀₀ = a₂₀₂}
        {p₁₀₂ : a₀₀₂ = a₂₀₂} {p₀₁₂ : a₀₀₂ = a₀₂₂} {p₀₂₁ : a₀₂₀ = a₀₂₂}
@@ -60,12 +59,32 @@ namespace eq
 
   definition rfl3 : cube hrfl hrfl hrfl hrfl s₁₀₁ s₁₀₁ := !refl3
 
+  -- Variables for composition
+  variables {a₄₀₀ a₄₀₂ a₄₂₀ a₄₂₂ : A}
+    {p₃₀₀ : a₂₀₀ = a₄₀₀} {p₃₀₂ : a₂₀₂ = a₄₀₂} {p₃₂₀ : a₂₂₀ = a₄₂₀} {p₃₂₂ : a₂₂₂ = a₄₂₂}
+    {p₄₀₁ : a₄₀₀ = a₄₀₂} {p₄₁₀ : a₄₀₀ = a₄₂₀} {p₄₁₂ : a₄₀₂ = a₄₂₂} {p₄₂₁ : a₄₂₀ = a₄₂₂}
+    {s₃₀₁ : square p₃₀₀ p₃₀₂ p₂₀₁ p₄₀₁}
+    {s₃₁₀ : square p₂₁₀ p₄₁₀ p₃₀₀ p₃₂₀}
+    {s₃₁₂ : square p₂₁₂ p₄₁₂ p₃₀₂ p₃₂₂}
+    {s₃₂₁ : square p₃₂₀ p₃₂₂ p₂₂₁ p₄₂₁}
+    {s₄₁₁ : square p₄₁₀ p₄₁₂ p₄₀₁ p₄₂₁}
+    (d : cube s₃₁₀ s₃₁₂ s₂₁₁ s₄₁₁ s₃₀₁ s₃₂₁)
+
+  /- Composition of Cubes -/
+
+  include c d
+  definition concat1 : cube (s₁₁₀ ⬝h s₃₁₀) _ s₀₁₁ s₄₁₁ _ _ :=
+  begin
+
+  end
+
+  omit c d
+
   definition eq_of_cube (c : cube s₁₁₀ s₁₁₂ s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁) :
     transpose s₁₀₁⁻¹ᵛ ⬝h s₁₁₀ ⬝h transpose s₁₂₁ =
       whisker_square (eq_bot_of_square s₀₁₁) (eq_bot_of_square s₂₁₁) idp idp s₁₁₂ :=
   by induction c; reflexivity
 
-  --set_option pp.implicit true
   definition eq_of_vdeg_cube {s s' : square p₀₁₀ p₂₁₀ p₁₀₀ p₁₂₀}
     (c : cube s s' vrfl vrfl vrfl vrfl) : s = s' :=
   begin
diff --git a/hott/cubical/square.hlean b/hott/cubical/square.hlean
index e7b443b95..cd86bc382 100644
--- a/hott/cubical/square.hlean
+++ b/hott/cubical/square.hlean
@@ -500,8 +500,12 @@ namespace eq
   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  :=
+  definition square_Flr_ap_idp {A B : Type} {b : B} {f : A → B} (p : Π a, f a = b)
+    {a b : A} (q : a = b) : square (p a) (p b) (ap f q) idp  :=
   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
+
 end eq
diff --git a/hott/homotopy/join.hlean b/hott/homotopy/join.hlean
index f5f7146ed..f115ca5ba 100644
--- a/hott/homotopy/join.hlean
+++ b/hott/homotopy/join.hlean
@@ -97,7 +97,7 @@ namespace join
 
   variables {A B C : Type}
 
-  private definition switch_left : join A B → join (join C B) A :=
+  private definition switch_left [reducible] : 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
@@ -112,10 +112,10 @@ namespace join
   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,
+    apply !switch_coh_fill.1,
   end
 
-  protected definition switch : join (join A B) C → join (join C B) A :=
+  protected definition switch [reducible] : 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,
@@ -136,7 +136,43 @@ namespace join
     square idp idp (ap !(@join.switch C B) (switch_coh (inl a) c)) (jglue (inl a) c) :=
   begin
     refine hrfl ⬝h _,
-    refine 
+    refine aps join.switch hrfl ⬝h _, esimp[switch_coh],
+    refine hdeg_square !ap_inv ⬝h _,
+    refine hrfl⁻¹ʰ⁻¹ᵛ ⬝h _, esimp[join.switch,switch_left],
+    refine (hdeg_square !elim_glue)⁻¹ᵛ ⬝h _,
+    refine hrfl⁻¹ᵛ ⬝h _, apply hdeg_square !inv_inv,
+  end
+
+  private definition switch_inv_coh_right (c : C) (b : B) :
+    square idp idp (ap !(@join.switch _ _ A) (switch_coh (inr b) c)) (jglue (inr b) c) :=
+  begin
+    refine hrfl ⬝h _,
+    refine aps join.switch hrfl ⬝h _, esimp[switch_coh],
+    refine aps join.switch (hdeg_square !ap_inv) ⬝h _,
+    refine hdeg_square !ap_inv ⬝h _,
+    refine (hdeg_square !ap_compose)⁻¹ᵛ⁻¹ʰ ⬝h _,
+    refine hrfl⁻¹ᵛ ⬝h _, esimp[join.switch,switch_left],
+    refine (hdeg_square !elim_glue)⁻¹ᵛ ⬝h _, apply hdeg_square !inv_inv,
+  end
+
+  private definition switch_inv_left (ab : join A B) :
+    !(@join.switch C) (join.switch (inl ab)) = inl ab :=
+  begin
+    induction ab with a b, do 2 reflexivity,
+    induction x with a b, apply eq_pathover, exact !switch_inv_left_square,
+  end
+
+  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) :
+    cube ids (switch_inv_left_square a b)
+      (square_Fl_Fl_ap_idp _ _) (square_Fl_Fl_ap_idp _ _)
+      --(switch_inv_coh_left c a) (switch_inv_coh_right c b)
+      :=
+  begin
+
   end