From 9d562c1e5d1c7d91a06b6c2b33b437d973897b2d Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Sat, 1 Jul 2017 17:13:29 +0100
Subject: [PATCH] working on the left inverse of a spectral equivalence

---
 homotopy/pointed_cubes.hlean | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)

diff --git a/homotopy/pointed_cubes.hlean b/homotopy/pointed_cubes.hlean
index 02021f0..878bd3b 100644
--- a/homotopy/pointed_cubes.hlean
+++ b/homotopy/pointed_cubes.hlean
@@ -96,3 +96,25 @@ phsquare (pwhisker_left fright phtpy_top) (pwhisker_right fleft phtpy_bot) psq_b
 
 definition ptube_h {A B C D : Type*} {ftop : A →* B} {fbot : C →* D} {fleft fleft' : A →* C} (phtpy_left : fleft ~* fleft') {fright fright' : B →* D} (phtpy_right : fright ~* fright') (psq_back : psquare ftop fbot fleft fright) (psq_front : psquare ftop fbot fleft' fright') : Type :=
 phsquare (pwhisker_right ftop phtpy_right) (pwhisker_left fbot phtpy_left) psq_back psq_front
+
+print pinv_right_phomotopy_of_phomotopy
+
+definition psquare_inv_top_bot {A B C D : Type*} {ftop : A ≃* B} {fbot : C ≃* D} {fleft : A →* C} {fright : B →* D} (psq : psquare ftop fbot fleft fright) : psquare ftop⁻¹ᵉ* fbot⁻¹ᵉ* fright fleft :=
+begin
+  fapply psquare_of_phomotopy,
+  refine (pinv_right_phomotopy_of_phomotopy _),
+  refine _ ⬝* (passoc fbot⁻¹ᵉ* fright ftop)⁻¹*,
+  refine (pinv_left_phomotopy_of_phomotopy _)⁻¹*,
+  exact psq,
+end
+
+definition ptube_v_left_inv {A B C D : Type*} {ftop : A ≃* B} {fbot : C ≃* D} {fleft : A →* C} {fright : B →* D} 
+  (psq : psquare ftop fbot fleft fright) : 
+  ptube_v 
+    (pleft_inv ftop) 
+    (pleft_inv fbot) 
+    (psquare_hcompose psq (psquare_inv_top_bot psq)) 
+    (psquare_of_pid_top_bot phomotopy.rfl) :=
+begin
+  exact sorry
+end