From bd064ef9c802fe3e8430d1cbb250f18301ade4c3 Mon Sep 17 00:00:00 2001
From: Jakob von Raumer <javra@web.de>
Date: Wed, 25 Nov 2015 18:16:02 +0000
Subject: [PATCH] feat(hott/homotopy): prove missing helper lemmas up to cube
 massaging

---
 hott/cubical/square.hlean |  6 ++++++
 hott/homotopy/join.hlean  | 19 +++++++++----------
 2 files changed, 15 insertions(+), 10 deletions(-)

diff --git a/hott/cubical/square.hlean b/hott/cubical/square.hlean
index d96498b31..af16b676d 100644
--- a/hott/cubical/square.hlean
+++ b/hott/cubical/square.hlean
@@ -46,6 +46,12 @@ namespace eq
   definition vdeg_square [unfold 6] {p q : a = a'} (r : p = q) : square p q idp idp :=
   by induction r;apply vrefl
 
+  definition hdeg_square_idp (p : a = a') : hdeg_square (refl p) = hrfl :=
+  by cases p; reflexivity
+  
+  definition vdeg_square_idp (p : a = a') : vdeg_square (refl p) = vrfl :=
+  by cases p; reflexivity
+
   definition hconcat [unfold 16] (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) (s₃₁ : square p₃₀ p₃₂ p₂₁ p₄₁)
     : square (p₁₀ ⬝ p₃₀) (p₁₂ ⬝ p₃₂) p₀₁ p₄₁ :=
   by induction s₃₁; exact s₁₁
diff --git a/hott/homotopy/join.hlean b/hott/homotopy/join.hlean
index eaf6dc4d3..380a67128 100644
--- a/hott/homotopy/join.hlean
+++ b/hott/homotopy/join.hlean
@@ -128,7 +128,7 @@ namespace join
     (c : cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂) :
     cube s₁₁₂⁻¹ᵛ vrfl (massage_sq s₁₀₁) (massage_sq s₁₂₁) s₁₁₀⁻¹ᵛ s₀₁₁⁻¹ᵛ :=
   begin
-    unfold massage_sq, exact sorry
+    exact sorry,
   end
 
   private definition massage_massage {A : Type} {a₀₀ a₀₂ a₂₀ : A}
@@ -226,11 +226,12 @@ namespace join
     (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
+    cases p, esimp at *, apply concat, apply inverse, apply vdeg_square_idp,
+    apply concat, apply ap vdeg_square, exact ap eq_of_pathover_idp q,
+    krewrite (is_equiv.right_inv (equiv.to_fun !pathover_idp)),
+    exact is_equiv.left_inv (equiv.to_fun (vdeg_square_equiv _ _)) sq,
   end
 
-  --set_option pp.implicit true
-
   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) :=
@@ -282,12 +283,10 @@ namespace join
     (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),
+    cases q, esimp at *, apply concat, apply inverse, apply vdeg_square_idp,
+    apply concat, apply ap vdeg_square, apply ap eq_of_pathover_idp e,
+    krewrite (is_equiv.right_inv (equiv.to_fun !pathover_idp)),
+    exact is_equiv.left_inv (equiv.to_fun (vdeg_square_equiv _ _)) sq,
   end
 
   private definition switch_inv_coh (c : C) (k : join A B) :