mark postulates so I can see what is left

badpostulates

@@ -1,6 +1,10 @@
-# exclude any directories named "scraps" or "in-progress"
+# excludes:
+# - oldlib
+# - misc
+# - any directories named "scraps" or "in-progress";
+# things from these directories should not be imported by anything else!
 
 #!/bin/bash
 
-find . -name "*.agda" | grep -v "oldlib" | xargs grep postulate | grep -v "HoTT Axiom" | grep -v "Agda Primitive"  | grep -v "scraps" | grep -v "in-progress" 
+find . -name "*.agda" | grep -v "oldlib" | xargs grep postulate | grep -v "misc" | grep -v "HoTT Axiom" | grep -v "Agda Primitive"  | grep -v "scraps" | grep -v "in-progress" 
 

categories/Infinity1-2.agda

@@ -4,7 +4,8 @@ open import lib.Prelude
 
 module categories.Infinity1-2 where
 
-  postulate 
+  postulate {- HoTT Axiom -}
+  -- well not really HoTT, but it's a reasonable axiom
     parametricity : {A B : Type} (f : (X : Type) → (B → X) → (A → X)) 
                   → (X : _) (k : B → X) → f X k == \ a -> k (f B (\ x -> x) a)
 

categories/Infinity1-ByHand.agda

@@ -4,16 +4,17 @@ open import lib.Prelude
 
 module categories.Infinity1-ByHand where
 
-  postulate 
+  postulate {- HoTT Axiom -}
+  -- well not really HoTT, but it's a reasonable axiom
     parametricity : {A B : Type} (f : (X : Type) → (B → X) → (A → X)) 
                   → (X : _) (k : B → X) → f X k == \ a -> k (f B (\ x -> x) a)
 
     parametricity-comp : {A B : Type} (f : (X : Type) → (B → X) → (A → X)) 
                        → parametricity f B (\ x -> x) == id 
 
-  -- postulate Π≃β2 : {A : Type} {B : A → Type} {C : (a : A) → B a → Type}
-  --                (f : (x : A) → (b : B a) → C a b)
-  --                → ap f  
+  -- Π≃β2 : {A : Type} {B : A → Type} {C : (a : A) → B a → Type}
+  --        (f : (x : A) → (b : B a) → C a b)
+  --        → ap f  
 
   data Glob (A B : Type) : Type
   T : {A B : Type} → Glob A B -> Type

categories/Infinity1.agda

@@ -4,7 +4,8 @@ open import lib.Prelude
 
 module categories.Infinity1 where
 
-  postulate 
+  postulate {-# HoTT Axiom #-}
+  -- well not really HoTT, but it's a reasonable axiom
     parametricity : {A B : Type} (f : (X : Type) → (B → X) → (A → X)) 
                   → (X : _) (k : B → X) → f X k == \ a -> k (f B (\ x -> x) a)
 

categories/Infinity1Diag.agda

@@ -90,7 +90,9 @@ module categories.Infinity1Diag where
 
   -- end mutual
 
-  postulate EQ : {A : Type} {M N : A} → M ≃ N
+  EQ : {A : Type} {M N : A} → M ≃ N
+  EQ = {!!}
+
 
 
   interp-diag : Diag → Type

computational-interp/ArrowFill.agda

@@ -0,0 +1,29 @@
+{-# OPTIONS --type-in-type --without-K #-}
+
+open import lib.Prelude
+open import lib.cubical.Cubical
+
+module computational-interp.ArrowFill where
+
+  coe→ : {A0 A1 B0 B1 : Type} (A : A0 == A1) (B : B0 == B1) (f : A0 -> B0)
+       → coe (ap (\ XY → fst XY → snd XY) (pair×≃ A B)) f == \ a1 → coe B (f (coe (! A) a1))
+  coe→ id id f = id
+
+  fill→ : {A0 A1 B0 B1 : Type} (A : A0 == A1) (B : B0 == B1) (f : A0 -> B0)
+         → PathOver (\ X → X)
+                    (ap (\ XY → fst XY → snd XY) (pair×≃ A B))
+                    f
+                    (\ a1 → coe B (f (coe (! A) a1)))
+  fill→ {A0}{A1} A B f =
+    over-o-ap (λ X → X) {δ' = pair×≃ A B} 
+      (in-PathOverΠ (λ a0 a1 α → 
+        over-ap-o (λ X → X) (changeover (λ X → X) (! red2) 
+          (PathOver-transport-right' (λ X → X) B (ap f (over-to-hom/right α) · red1))))) where
+        red1 : {a1 : _} → 
+               (f (transport (λ v → fst v) (! (pair×≃ A B)) a1)) == 
+               f (coe (! A) a1)
+        red1 = {!!}
+
+        red2 : ∀ {a0 : A0} {a1 : A1} {α : PathOver (λ v → fst v) (pair×≃ A B) a0 a1} 
+                → (ap (λ z → snd (fst z)) (pair= (pair×≃ A B) α)) == B
+        red2 = {!!}

computational-interp/GCube.agda

@@ -1,7 +1,7 @@
 {-# OPTIONS --type-in-type --without-K #-}
 
 open import lib.Prelude
-open import lib.PathOver
+open import lib.cubical.PathOver
 
 module computational-interp.GCube where
 
@@ -21,8 +21,8 @@ module computational-interp.GCube where
 
     d n (B , _) = B
 
-    postulate 
-      InsideS : (n : Nat) → (c1 : Cube n) → (c2 : Cube n) → BoundaryPath n (d n c1) (d n c2) → Type
+    InsideS : (n : Nat) → (c1 : Cube n) → (c2 : Cube n) → BoundaryPath n (d n c1) (d n c2) → Type
+    InsideS = {!!}
 
     Inside Z <> = A
     Inside (S n) (c1 , c2 , p) = InsideS n c1 c2 p

computational-interp/GCube2.agda

@@ -1,7 +1,7 @@
 {-# OPTIONS --type-in-type --without-K #-}
 
 open import lib.Prelude
-open import lib.PathOver
+open import lib.cubical.PathOver
 
 module computational-interp.GCube2 where
 
@@ -35,8 +35,8 @@ module computational-interp.GCube2 where
 
     d n (B , _) = B
 
-    postulate 
-      InsideS : (n : Nat) → (c1 : Cube n) → (c2 : Cube n) → BoundaryPath n (d n c1) (d n c2) → Type
+    InsideS : (n : Nat) → (c1 : Cube n) → (c2 : Cube n) → BoundaryPath n (d n c1) (d n c2) → Type
+    InsideS = {!!}
 
     Inside Z <> = A
     Inside (S n) (c1 , c2 , p) = InsideS n c1 c2 p

computational-interp/hcanon/HSetLang-PathOver.agda → computational-interp/scraps/hcanon/HSetLang-PathOver.agda

@@ -1,7 +1,7 @@
 {-# OPTIONS --type-in-type --no-termination-check #-}
 
 open import lib.Prelude 
-open import lib.PathOver
+open import lib.cubical.PathOver
 open BoolM 
 import lib.PrimTrustMe
 
@@ -183,8 +183,8 @@ module computational-interp.hcanon.HSetLang-PathOver where
   -- interp-plam M θ = λ x → interp M (θ , x)
   -- interp-papp M N θ = interp M θ (interp N θ)
   interp-uap-eqv f g θ = (improve (hequiv (λ x → interp f (θ , x)) (λ y → interp g (θ , y)) FIXME1 FIXME2))  where
-    postulate FIXME1 : _
-              FIXME2 : _
+    postulate FIXME1 : _ 
+              FIXME2 : _ 
     -- one option would be to observe that all props are hprops, but what goes wrong if we don't?
   -- interp-lam= f g α θ = λ≃ (λ x → interp α (θ , x))
 

computational-interp/hcanon/HSetLang-Telescope.agda → computational-interp/scraps/hcanon/HSetLang-Telescope.agda

@@ -176,8 +176,8 @@ module computational-interp.hcanon.HSetLang-Telescope2 where
   interp-plam M θ = λ x → interp M (θ , x)
   interp-papp M N θ = interp M θ (interp N θ)
   interp-uap-eqv f g θ = (improve (hequiv (λ x → interp f (θ , x)) (λ y → interp g (θ , y)) FIXME1 FIXME2))  where
-    postulate FIXME1 : _
-              FIXME2 : _
+    postulate FIXME1 : _ 
+              FIXME2 : _ 
     -- one option would be to observe that all props are hprops, but what goes wrong if we don't?
   interp-lam= f g α θ = λ≃ (λ x → interp α (θ , x))
 

computational-interp/hcanon/HSetLang.agda → computational-interp/scraps/hcanon/HSetLang.agda

@@ -175,8 +175,8 @@ module computational-interp.hcanon.HSetLang where
   -- interp-plam M θ = λ x → interp M (θ , x)
   -- interp-papp M N θ = interp M θ (interp N θ)
   interp-uap-eqv f g θ = (improve (hequiv (λ x → interp f (θ , x)) (λ y → interp g (θ , y)) FIXME1 FIXME2))  where
-    postulate FIXME1 : _
-              FIXME2 : _
+    postulate FIXME1 : _ 
+              FIXME2 : _ 
     -- one option would be to observe that all props are hprops, but what goes wrong if we don't?
   interp-lam= f g α θ = λ≃ (λ x → interp α (θ , x))
 

computational-interp/hcanon/HSetProof-PathOver.agda → computational-interp/scraps/hcanon/HSetProof-PathOver.agda

@@ -101,7 +101,7 @@ module computational-interp.hcanon.HSetProof-PathOver where
             (eq : δ == δ')
             (rα : QOver rδ A* rM1 rM2 α)
             → QOver rδ' A* rM1 rM2 (changeover A eq α)
-  postulate 
+  postulate --in-progress
     fund-transport : ∀ {Γ' C θ1 θ2 δ N} (Γ'* : Ctx Γ') (C* : Ty Γ'* C) 
               (rθ1 : RC Γ'* θ1) (rθ2 : RC Γ'* θ2) 
               (rδ : QC Γ'* rθ1 rθ2 δ) 

computational-interp/hcanon/HSetProof-binaryQPi.agda → computational-interp/scraps/hcanon/HSetProof-binaryQPi.agda

@@ -83,7 +83,7 @@ module computational-interp.hcanon.HSetProof3 where
              → Q Γ* A* rθ rN rO β
              → Q Γ* A* rθ rM rO (β ∘ α)
 
-  postulate -- PERF
+  postulate -- PERF 
     transportR : ∀ {Γ A θ M M'} (Γ* : Ctx Γ) (A* : Ty Γ* A) (rθ : RC Γ* θ) → M == M' → 
                R Γ* A* rθ M → R Γ* A* rθ M'
     transportQ : ∀ {Γ A} (Γ* : Ctx Γ) (A* : Ty Γ* A) → {θ : Γ} → (rθ : RC Γ* θ) 

computational-interp/ua-implies-funext/Stream.agda

@@ -17,7 +17,8 @@ module Stream where
   head (map f s) = f (head s)
   tail (map f s) = map f (tail s)
 
-  postulate 
+  postulate {- HoTT Axiom -}
+  -- well not really HoTT, but an axiom
     map-id : {A : Type} → map {A} (\ x -> x) == (\ s -> s)
     map-o  : {A B C : Type} (g : B → C) (f : A → B) → map g o map f == map (g o f)
 

computational-interp/ua-implies-funext/Stream2.agda

@@ -23,7 +23,8 @@ module Stream2 where
   head (map f s) = f (head s)
   tail (map f s) = map f (tail s)
 
-  postulate 
+  postulate {-# HoTT Axiom #-}
+  -- well not really HoTT...
     map-id : {A : Type} → map {A} (\ x -> x) == (\ s -> s)
     map-o  : {A B C : Type} (g : B → C) (f : A → B) (s : Stream A) → map g (map f s) == map (g o f) s
 
@@ -88,11 +89,11 @@ module Stream2 where
   Bisim-tails : {A : Type} {xs ys : Stream A} → Bisim xs ys → Bisim (tail xs) (tail ys)
   Bisim-tails (ps , (id , id)) = (tail ps , id , id)
 
-  postulate
-    Bisim-unfold : {A : Type} (X : Stream A → Stream A → Type)
+  Bisim-unfold : {A : Type} (X : Stream A → Stream A → Type)
                → (∀ xs ys → X xs ys → ((head xs) == (head ys)) × X (tail xs) (tail ys))
                → ∀ (xs ys : Stream A) → X xs ys → Bisim xs ys
-
+  Bisim-unfold = {!!}
+
   unfoldη : {A : Type} {X : Type} (f : X → A × X) (s : X → Stream A)
              → ((x : X) → head (s x) == fst (f x))
              → ((x : X) → tail (s x) == s (snd (f x)))

homotopy/blakersmassey/ooTopos.agda

@@ -10,14 +10,6 @@ module homotopy.blakersmassey.ooTopos (X Y : Type) (P : X → Y → Type)
                                       (cf : (x : X) → Connected (S i') (Σ \ y → P x y))
                                       (cg : (y : Y) → Connected (S j') (Σ \ x → P x y)) where 
 
-  -- trivial by equiv induction, but easier if it computes
-  HFiber-at-equiv : ∀ {A B B'} (e : Equiv B B') (f : A → B') {b : B}
-                  → Equiv (HFiber f (fst e b)) (HFiber (IsEquiv.g (snd e) o f) b)
-  HFiber-at-equiv e f {b} = improve (hequiv (λ p → (fst p) , {!snd p!}) {!!} {!!} {!!})
-
-  post∘-equiv : ∀ {A} {a1 a2 a3 : A} (p : a2 == a3) → Equiv (a1 == a2) (a1 == a3)
-  post∘-equiv p = improve (hequiv (λ x → p ∘ x) (λ x → ! p ∘ x) {!!} {!!})
-
   i : TLevel
   i = S i'
 
@@ -91,7 +83,7 @@ module homotopy.blakersmassey.ooTopos (X Y : Type) (P : X → Y → Type)
                                         w
 
     switchr-twice : ∀ z w → switchr (switchr (z , w)) == (z , w)
-    switchr-twice z = Wedge.Pushout-elim _ (λ _ → id) (λ _ → id) (λ _ → {!!})
+    switchr-twice z = Wedge.Pushout-elim _ (λ _ → id) (λ _ → id) (λ _ → PathOver=.in-PathOver-= {!!})
 
     switchr-equiv : Equiv (Σ \ (z : Z) → Z×X-∨-×YZ (snd z)) (Σ \ (z : Z) → Z×X-∨-×YZ (snd z))
     switchr-equiv = improve (hequiv switchr switchr (\ p → switchr-twice (fst p) (snd p)) (\ p → switchr-twice (fst p) (snd p)))
@@ -119,9 +111,14 @@ module homotopy.blakersmassey.ooTopos (X Y : Type) (P : X → Y → Type)
 
     m-to-ml-triangle : ∀ z (w : Z×X-∨-×YZ (snd z)) → (glueml-total o m-to-ml) (z , w) == gluem-total (z , w)
     m-to-ml-triangle z = Wedge.Pushout-elim (λ w → (glueml-total o m-to-ml) (z , w) == gluem-total (z , w))
-                                            (λ yp → ap (λ Q → z , ((fst (fst z) , fst yp) , snd yp) , Q) {!!})
-                                            (λ xp → ap (λ Q → z , ((fst xp , snd (fst z)) , snd xp) , Q) {!!})
-                                            {!!}
+                                            (λ yp → ap (λ Q → z , ((fst (fst z) , fst yp) , snd yp) , Q) (coh1 (gluel (snd yp)) (gluel (snd z)) (gluer (snd z))))
+                                            (λ xp → ap (λ Q → z , ((fst xp , snd (fst z)) , snd xp) , Q) (coh2 (gluel (snd xp)) (gluer (snd xp)) (gluer (snd z))))
+                                            (λ _ → PathOver=.in-PathOver-= {!seems annoying!}) where
+      coh1 : ∀ {A} {a0 a1 a2 a3 : A} (lyp : a0 == a1) (lz : a2 == a1) (rz : a2 == a3) → (! lyp ∘ ! (rz ∘ ! (lz)) ∘ rz) == (! lyp ∘ lz)
+      coh1 id id id = id
+
+      coh2 : ∀ {A} {a0 a1 a2 a3 : A} (lxp : a0 == a1) (rxp : a0 == a2) (rz : a3 == a2) → (! lxp ∘ ! (rxp ∘ ! (lxp)) ∘ rz) == (! rxp ∘ rz)
+      coh2 id id id = id
 
     gluemr-total : 〈Z×Z〉×〈XY〉Z → Z×WZ
     gluemr-total = (fiberwise-to-total (\ (ppp0 : Z) → (fiberwise-to-total (\ (ppxy : Z) → gluemr (snd ppp0) (snd ppxy)))))

lib/AdjointEquiv.agda

@@ -12,6 +12,7 @@ module lib.AdjointEquiv where
  id-equiv : ∀ {A} -> Equiv A A
  id-equiv = ( (\ x -> x) , isequiv (λ x → x) (\ _ -> id) (\ _ -> id) (\ _ -> id))
 
+ -- NOTE: because this just flips the first four, IsEquiv.γ (!equiv e) works as a name for the other ("sixth") triangle equality for e
  !equiv : ∀ {A B} → Equiv A B → Equiv B A
  !equiv (f , isequiv g α β γ) = 
    equiv g f β α 

lib/Char.agda

@@ -32,7 +32,9 @@ module lib.Char where
 
   equals : (c d : Char) → Either (c == d) (c == d → Void)
   equals c d with equal c d
-  ... | True = Inl FIXME where
-    postulate FIXME : {A : Set} → A
-  ... | False = Inr (\ _ -> FIXME) where
-    postulate FIXME : {A : Set} → A
+  ... | True = Inl CharEq where
+    postulate {- Agda Primitive, not really we can't use primTrustMe without using universe levels -}
+      CharEq : c == d 
+  ... | False = Inr (\ _ -> CharsNeq) where
+    postulate {- Agda Primitive, not really, but how are you supposed to do this? -}
+      CharsNeq : Void

lib/HFiber.agda

@@ -7,6 +7,7 @@ open import lib.Sums
 open import lib.Prods
 open import lib.Paths
 open import lib.NType
+open import lib.AdjointEquiv
 open import lib.cubical.PathOver
 
 module lib.HFiber where
@@ -30,6 +31,33 @@ module lib.HFiber where
   hfiber-fst : ∀ {A} {B : A → Type} (a : A) → (B a) == (HFiber {Σ B} fst a)
   hfiber-fst {B = B} a = ua (hfiber-fst-eqv a)
 
+  HFiber-at-equiv : ∀ {A B B'} (e : Equiv B B') (f : A → B') {b : B}
+                  → Equiv (HFiber f (fst e b)) (HFiber (IsEquiv.g (snd e) o f) b)
+  HFiber-at-equiv e f {b} = 
+    improve (hequiv (λ p → (fst p) , IsEquiv.α (snd e) b ∘ ap (IsEquiv.g (snd e)) (snd p))
+                    (λ p → (fst p) , (ap (fst e) (snd p) ∘ ! (IsEquiv.β (snd e) (f (fst p)))))
+                    (λ hf → ap (λ Z₁ → fst hf , Z₁)
+                          (ap (fst e) (IsEquiv.α (snd e) b ∘ ap (IsEquiv.g (snd e)) (snd hf)) ∘ ! (IsEquiv.β (snd e) (f (fst hf))) ≃〈 ap (λ Z₁ → Z₁ ∘ ! (IsEquiv.β (snd e) (f (fst hf)))) (ap-∘ (fst e) (IsEquiv.α (snd e) b) (ap (IsEquiv.g (snd e)) (snd hf))) 〉 
+                           (ap (fst e) (IsEquiv.α (snd e) b) ∘ ap (fst e) (ap (IsEquiv.g (snd e)) (snd hf))) ∘ ! (IsEquiv.β (snd e) (f (fst hf))) ≃〈 ! (∘-assoc (ap (fst e) (IsEquiv.α (snd e) b)) (ap (fst e) (ap (IsEquiv.g (snd e)) (snd hf))) (! (IsEquiv.β (snd e) (f (fst hf))))) 〉 
+                           ap (fst e) (IsEquiv.α (snd e) b) ∘ ap (fst e) (ap (IsEquiv.g (snd e)) (snd hf)) ∘ ! (IsEquiv.β (snd e) (f (fst hf))) ≃〈 ap (λ Z₁ → Z₁ ∘ ap (fst e) (ap (IsEquiv.g (snd e)) (snd hf)) ∘ ! (IsEquiv.β (snd e) (f (fst hf)))) (! (IsEquiv.γ (snd e) b)) 〉 
+                           IsEquiv.β (snd e) (fst e b) ∘ ap (fst e) (ap (IsEquiv.g (snd e)) (snd hf)) ∘ ! (IsEquiv.β (snd e) (f (fst hf))) ≃〈 ap (λ Z₁ → IsEquiv.β (snd e) (fst e b) ∘ Z₁ ∘ ! (IsEquiv.β (snd e) (f (fst hf)))) (! (ap-o (fst e) (IsEquiv.g (snd e)) (snd hf)))  〉
+                           IsEquiv.β (snd e) (fst e b) ∘ ap (fst e o IsEquiv.g (snd e)) (snd hf) ∘ ! (IsEquiv.β (snd e) (f (fst hf))) ≃〈 ap (λ Z₁ → IsEquiv.β (snd e) (fst e b) ∘ Z₁ ∘ ! (IsEquiv.β (snd e) (f (fst hf)))) (ap-by-id (λ x → ! (IsEquiv.β (snd e) x)) (snd hf))  〉
+                           IsEquiv.β (snd e) (fst e b) ∘ (! (IsEquiv.β (snd e) (fst e b)) ∘ snd hf ∘ ! (! (IsEquiv.β (snd e) (f (fst hf))))) ∘ ! (IsEquiv.β (snd e) (f (fst hf))) ≃〈 assoc-131->right (IsEquiv.β (snd e) (fst e b)) (! (IsEquiv.β (snd e) (fst e b))) (snd hf) (! (! (IsEquiv.β (snd e) (f (fst hf))))) (! (IsEquiv.β (snd e) (f (fst hf))))  〉
+                           IsEquiv.β (snd e) (fst e b) ∘ ! (IsEquiv.β (snd e) (fst e b)) ∘ snd hf ∘ ! (! (IsEquiv.β (snd e) (f (fst hf)))) ∘ ! (IsEquiv.β (snd e) (f (fst hf))) ≃〈 !-inv-r-front (IsEquiv.β (snd e) (fst e b)) (snd hf ∘ ! (! (IsEquiv.β (snd e) (f (fst hf)))) ∘ ! (IsEquiv.β (snd e) (f (fst hf))))  〉
+                           snd hf ∘ ! (! (IsEquiv.β (snd e) (f (fst hf)))) ∘ ! (IsEquiv.β (snd e) (f (fst hf))) ≃〈 !-inv-l-back (snd hf) (! (IsEquiv.β (snd e) (f (fst hf)))) 〉 
+                           snd hf ∎))
+                    (\ hc → ap (λ Z₁ → fst hc , Z₁) 
+                               (IsEquiv.α (snd e) b ∘ ap (IsEquiv.g (snd e)) (ap (fst e) (snd hc) ∘ ! (IsEquiv.β (snd e) (f (fst hc)))) ≃〈 ap (λ Z₁ → IsEquiv.α (snd e) b ∘ Z₁) (ap-∘ (IsEquiv.g (snd e)) (ap (fst e) (snd hc)) (! (IsEquiv.β (snd e) (f (fst hc))))) 〉 
+                                IsEquiv.α (snd e) b ∘ ap (IsEquiv.g (snd e)) (ap (fst e) (snd hc)) ∘ ap (IsEquiv.g (snd e)) (! (IsEquiv.β (snd e) (f (fst hc)))) ≃〈 ap (λ Z₁ → IsEquiv.α (snd e) b ∘ Z₁ ∘ ap (IsEquiv.g (snd e)) (! (IsEquiv.β (snd e) (f (fst hc))))) (! (ap-o (IsEquiv.g (snd e)) (fst e) (snd hc))) 〉 
+                                IsEquiv.α (snd e) b ∘ ap (IsEquiv.g (snd e) o (fst e)) (snd hc) ∘ ap (IsEquiv.g (snd e)) (! (IsEquiv.β (snd e) (f (fst hc)))) ≃〈 ap (λ Z₁ → IsEquiv.α (snd e) b ∘ Z₁ ∘ ap (IsEquiv.g (snd e)) (! (IsEquiv.β (snd e) (f (fst hc))))) (ap-by-id (λ x → ! (IsEquiv.α (snd e) x)) (snd hc)) 〉 
+                                IsEquiv.α (snd e) b ∘ (! (IsEquiv.α (snd e) b) ∘ snd hc ∘ ! (! (IsEquiv.α (snd e) (IsEquiv.g (snd e) (f (fst hc)))))) ∘ ap (IsEquiv.g (snd e)) (! (IsEquiv.β (snd e) (f (fst hc))))  ≃〈 assoc-131->right (IsEquiv.α (snd e) b) (! (IsEquiv.α (snd e) b)) (snd hc) (! (! (IsEquiv.α (snd e) (IsEquiv.g (snd e) (f (fst hc)))))) (ap (IsEquiv.g (snd e)) (! (IsEquiv.β (snd e) (f (fst hc))))) 〉 
+                                IsEquiv.α (snd e) b ∘ ! (IsEquiv.α (snd e) b) ∘ snd hc ∘ ! (! (IsEquiv.α (snd e) (IsEquiv.g (snd e) (f (fst hc))))) ∘ ap (IsEquiv.g (snd e)) (! (IsEquiv.β (snd e) (f (fst hc)))) ≃〈 !-inv-r-front (IsEquiv.α (snd e) b) (snd hc ∘ ! (! (IsEquiv.α (snd e) (IsEquiv.g (snd e) (f (fst hc))))) ∘ ap (IsEquiv.g (snd e)) (! (IsEquiv.β (snd e) (f (fst hc))))) 〉 
+                                snd hc ∘ ! (! (IsEquiv.α (snd e) (IsEquiv.g (snd e) (f (fst hc))))) ∘ ap (IsEquiv.g (snd e)) (! (IsEquiv.β (snd e) (f (fst hc)))) ≃〈 ap (λ Z₁ → snd hc ∘ ! (! (IsEquiv.α (snd e) (IsEquiv.g (snd e) (f (fst hc))))) ∘ Z₁) (ap-! (IsEquiv.g (snd e)) (IsEquiv.β (snd e) (f (fst hc)))) 〉 
+                                snd hc ∘ ! (! (IsEquiv.α (snd e) (IsEquiv.g (snd e) (f (fst hc))))) ∘ ! (ap (IsEquiv.g (snd e)) (IsEquiv.β (snd e) (f (fst hc)))) ≃〈 ap (λ Z₁ → snd hc ∘ Z₁ ∘ ! (ap (IsEquiv.g (snd e)) (IsEquiv.β (snd e) (f (fst hc))))) (!-invol (IsEquiv.α (snd e) (IsEquiv.g (snd e) (f (fst hc))))) 〉 
+                                snd hc ∘ (IsEquiv.α (snd e) (IsEquiv.g (snd e) (f (fst hc)))) ∘ ! (ap (IsEquiv.g (snd e)) (IsEquiv.β (snd e) (f (fst hc)))) ≃〈  ap (λ Z₁ → snd hc ∘ IsEquiv.α (snd e) (IsEquiv.g (snd e) (f (fst hc))) ∘ ! Z₁) (! (IsEquiv.γ (snd (!equiv e)) _)) 〉 
+                                snd hc ∘ IsEquiv.α (snd e) (IsEquiv.g (snd e) (f (fst hc))) ∘ ! (IsEquiv.α (snd e) (IsEquiv.g (snd e) (f (fst hc)))) ≃〈 !-inv-r-back (snd hc) (IsEquiv.α (snd e) (IsEquiv.g (snd e) (f (fst hc)))) 〉 
+                                snd hc ∎)))
+
   HFiber-fiberwise-to-total-eqv : {A : Type} {B C : A → Type} (f : (x : A) → B x → C x)
                                 → {a : A} {c : C a} → Equiv (HFiber (f a) c) (HFiber (fiberwise-to-total f) (a , c))
   HFiber-fiberwise-to-total-eqv {A}{B}{C} f {a}{c} =