closes #31

src/CubicalHott/Theorem7-1-8.agda

@@ -3,10 +3,15 @@
 module CubicalHott.Theorem7-1-8 where
 
 open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Equiv.Properties
 open import Cubical.Foundations.HLevels
 open import Cubical.Data.Sigma
 open import Data.Nat
 
+open import CubicalHott.Theorem2-7-2 renaming (theorem to theorem2-7-2)
+open import CubicalHott.Corollary7-1-5 renaming (corollary to corollary7-1-5)
+
 theorem : {A : Type} {B : A → Type} {n : ℕ}
   → isOfHLevel n A
   → ((a : A) → isOfHLevel n (B a))
@@ -25,16 +30,24 @@ theorem {A} {B} {suc zero} A-n-type B-n-type x @ (xa , xb) y @ (ya , yb) =
     let helper = J (λ a' p' → (ba' : B a') → PathP (λ i' → B (p' i')) xb ba') (λ ba' i' → B-n-type xa xb ba' i') (A-n-type xa ya) yb in
     helper i 
 theorem {A} {B} {2+ n} A-n-type B-n-type x @ (xa , xb) y @ (ya , yb) =
-  -- isOfHLevel (suc n) ((xa , xb) ≡ (ya , yb))
-  {!   !} where
-    goal : (p : xa ≡ ya) → isOfHLevel (suc n) (PathP (λ i → B (p i)) xb yb)
-    goal p = {!   !}
+  let eqv = theorem2-7-2 {w = x} {w' = y} in
+  let eqv2 = (fst invEquivEquiv) eqv in
+  let
+    IH = theorem (A-n-type xa ya)
+      -- (a : xa ≡ ya) → isOfHLevel (suc n) (PathP (λ i → B (a i)) xb yb)
+      λ p → J (λ a' p' → (yb' : B a') → isOfHLevel (suc n) (PathP (λ i → B (p' i)) xb yb')) (λ yb' → B-n-type xa xb yb') p yb
+  in corollary7-1-5 (suc n) eqv2 IH
 
-    IH = theorem
-      {A = xa ≡ ya}
-      {B = λ p → {!   !}}
-      {n = suc n}
-      (A-n-type xa ya)
-      {!   !}
+  -- -- isOfHLevel (suc n) ((xa , xb) ≡ (ya , yb))
+  -- {!   !} where
+  --   goal : (p : xa ≡ ya) → isOfHLevel (suc n) (PathP (λ i → B (p i)) xb yb)
+  --   goal p = {!   !}
 
-    IH' = subst (λ x₁ → {!   !}) {!   !} IH
+  --   IH = theorem
+  --     {A = xa ≡ ya}
+  --     {B = λ p → {!   !}}
+  --     {n = suc n}
+  --     (A-n-type xa ya)
+  --     {!   !}
+
+  --   IH' = subst (λ x₁ → {!   !}) {!   !} IH