From aa460fd5af21fb2da811e6e8af81cfacac2c1676 Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Sun, 20 Oct 2024 13:44:09 -0500
Subject: [PATCH] solve case 1 of theorem 7.1.11

---
 src/CubicalHott/Example3-6-2.agda  |  2 +-
 src/CubicalHott/Lemma3-11-4.agda   |  4 +-
 src/CubicalHott/Lemma3-5-1.agda    | 15 ++++++
 src/CubicalHott/Theorem7-1-10.agda |  2 +-
 src/CubicalHott/Theorem7-1-11.agda | 84 ++++++++++++++++++------------
 5 files changed, 71 insertions(+), 36 deletions(-)
 create mode 100644 src/CubicalHott/Lemma3-5-1.agda

diff --git a/src/CubicalHott/Example3-6-2.agda b/src/CubicalHott/Example3-6-2.agda
index 94954c2..632ac48 100644
--- a/src/CubicalHott/Example3-6-2.agda
+++ b/src/CubicalHott/Example3-6-2.agda
@@ -4,7 +4,7 @@ module CubicalHott.Example3-6-2 where
 
 open import Cubical.Foundations.Prelude
 
-example : {A : Type} → {B : A → Type}
+example : {l l2 : Level} → {A : Type l} → {B : A → Type l2}
   → ((x : A) → isProp (B x))
   → isProp ((x : A) → B x)
 example B-x-prop fx fy = λ i z → B-x-prop z (B-x-prop z (fx z) (fy z) i) (B-x-prop z (fx z) (fy z) i) i
\ No newline at end of file
diff --git a/src/CubicalHott/Lemma3-11-4.agda b/src/CubicalHott/Lemma3-11-4.agda
index 65e8af2..19672ce 100644
--- a/src/CubicalHott/Lemma3-11-4.agda
+++ b/src/CubicalHott/Lemma3-11-4.agda
@@ -5,8 +5,8 @@ module CubicalHott.Lemma3-11-4 where
 open import Cubical.Foundations.Prelude
 open import CubicalHott.Example3-6-2 renaming (example to example3-6-2)
 
-lemma : {A : Type} → isProp (isContr A)
-lemma {A} A-contr-x @ (x , px) (y , py) i =
+lemma : {l : Level} → {A : Type l} → isProp (isContr A)
+lemma {A = A} A-contr-x @ (x , px) (y , py) i =
   px y i , goal i where
     A-is-set = isProp→isSet (isContr→isProp A-contr-x)
 
diff --git a/src/CubicalHott/Lemma3-5-1.agda b/src/CubicalHott/Lemma3-5-1.agda
new file mode 100644
index 0000000..0dc936e
--- /dev/null
+++ b/src/CubicalHott/Lemma3-5-1.agda
@@ -0,0 +1,15 @@
+{-# OPTIONS --cubical #-}
+
+module CubicalHott.Lemma3-5-1 where
+
+open import Cubical.Foundations.Prelude
+
+lemma : {l l2 : Level} → {A : Type l} → {P : A → Type l2}
+  → ((x : A) → isProp (P x))
+  → (u v : Σ A P)
+  → (fst u ≡ fst v)
+  → u ≡ v
+lemma {P = P} Px-isProp u v p i = p i , goal i where
+  goal : PathP (λ i → P (p i)) (snd u) (snd v)
+  goal = toPathP (Px-isProp (fst v) (subst P p (snd u)) (snd v))
+  
\ No newline at end of file
diff --git a/src/CubicalHott/Theorem7-1-10.agda b/src/CubicalHott/Theorem7-1-10.agda
index 6d684fd..299a38a 100644
--- a/src/CubicalHott/Theorem7-1-10.agda
+++ b/src/CubicalHott/Theorem7-1-10.agda
@@ -8,7 +8,7 @@ open import Cubical.Data.Nat
 
 open import CubicalHott.Lemma3-11-4 renaming (lemma to lemma3-11-4)
 
-theorem : {X : Type} → (n : ℕ) → isProp (isOfHLevel n X)
+theorem : {l : Level} → {X : Type l} → (n : ℕ) → isProp (isOfHLevel n X)
 theorem zero = lemma3-11-4
 theorem (suc zero) isProp1 isProp2 i x y j = isProp→isSet isProp1 x y (isProp1 x y) (isProp2 x y) i j
 theorem {X = X} (suc (suc n)) isHLevel1 isHLevel2 =
diff --git a/src/CubicalHott/Theorem7-1-11.agda b/src/CubicalHott/Theorem7-1-11.agda
index ea14b3b..616c482 100644
--- a/src/CubicalHott/Theorem7-1-11.agda
+++ b/src/CubicalHott/Theorem7-1-11.agda
@@ -11,47 +11,67 @@ open import Cubical.Foundations.Univalence
 open import Cubical.Data.Nat
 open import Data.Unit
 
+open import CubicalHott.Lemma3-5-1 renaming (lemma to lemma3-5-1)
+open import CubicalHott.Theorem7-1-8 renaming (theorem to theorem7-1-8)
+open import CubicalHott.Theorem7-1-10 renaming (theorem to theorem7-1-10)
+
 lemma : ∀ {l} → (n : HLevel) → isOfHLevel (suc n) (TypeOfHLevel l n)
-lemma zero (A , a , Acontr) (B , b , Bcontr) i = A≡B i , a≡b i , λ y j → wtf i y j where
-  eqv1 : A ≃ B
-  eqv1 = isoToEquiv (iso (λ _ → b) (λ _ → a) Bcontr Acontr)
+lemma zero (A , a , Acontr) (B , b , Bcontr) i =
+  A≡B i , goal i where
+    -- isContr (A≡B i)
+    -- Acontr ≡ Bcontr
 
-  A≡B : A ≡ B
-  A≡B = ua eqv1
+    -- A≡B i , a≡b i , λ y j → wtf i y j where
+    eqv1 : A ≃ B
+    eqv1 = isoToEquiv (iso (λ _ → b) (λ _ → a) Bcontr Acontr)
 
-  a≡b : PathP (λ i → A≡B i) a b
-  a≡b j = glue (λ { (j = i0) → a ; (j = i1) → b }) b
+    A≡B : A ≡ B
+    A≡B = ua eqv1
 
-  -- eqv2 : ((y : A) → a ≡ y) ≡ ((y : B) → b ≡ y)
-  -- eqv2 = λ i → (y : A≡B i) → a≡b i ≡ y
+    a≡b : PathP (λ i → A≡B i) a b
+    a≡b j = glue (λ { (j = i0) → a ; (j = i1) → b }) b
 
-  -- T1 = λ { (i = i0) → ((y : A) → a ≡ y) ; (i = i1) → ((y : B) → b ≡ y) }
-  -- e1 = λ { (i = i0) → pathToEquiv eqv2 ; (i = i1) → idEquiv ((y : B) → b ≡ y) }
-  -- Uhh = primGlue ((y : B) → b ≡ y) T1 e1
-      
-  -- uhh : Uhh
-  -- uhh = glue {T = T1} {e = e1} (λ { (i = i0) → Acontr ; (i = i1) → Bcontr }) λ y j → {! Bcontr y j  !}
+    helper2 : (x : B) → isProp ((y : B) → x ≡ y)
+    helper2 x f1 f2 =
+      let helper = isProp→isSet (isContr→isProp (b , Bcontr)) in
+      funExt (λ (y : B) → helper x y (f1 y) (f2 y))
 
-  Acontr-is-Prop : isProp ((y : A) → a ≡ y)
+    helper : subst isContr A≡B (a , Acontr) ≡ (b , Bcontr)
+    helper = lemma3-5-1 helper2 (subst isContr A≡B (a , Acontr)) (b , Bcontr) (fromPathP a≡b)
 
-  wtf : PathP (λ i → (y : A≡B i) → a≡b i ≡ y) Acontr Bcontr
-  wtf = λ i y j → {!   !}
+    goal : PathP (λ i → isContr (A≡B i)) (a , Acontr) (b , Bcontr)
+    goal = toPathP helper
+
+    -- -- eqv2 : ((y : A) → a ≡ y) ≡ ((y : B) → b ≡ y)
+    -- -- eqv2 = λ i → (y : A≡B i) → a≡b i ≡ y
+
+    -- -- T1 = λ { (i = i0) → ((y : A) → a ≡ y) ; (i = i1) → ((y : B) → b ≡ y) }
+    -- -- e1 = λ { (i = i0) → pathToEquiv eqv2 ; (i = i1) → idEquiv ((y : B) → b ≡ y) }
+    -- -- Uhh = primGlue ((y : B) → b ≡ y) T1 e1
+        
+    -- -- uhh : Uhh
+    -- -- uhh = glue {T = T1} {e = e1} (λ { (i = i0) → Acontr ; (i = i1) → Bcontr }) λ y j → {! Bcontr y j  !}
+
+    -- Acontr-is-Prop : isProp ((y : A) → a ≡ y)
+
+    -- wtf : PathP (λ i → (y : A≡B i) → a≡b i ≡ y) Acontr Bcontr
+    -- wtf = λ i y j → {!   !}
 
 
-    -- a≡b i ≡ y
-    -- ———— Boundary (wanted) —————————————————————————————————————
-    -- i = i0 ⊢ λ i₁ → Acontr y i₁
-    -- i = i1 ⊢ λ i₁ → Bcontr y i₁
+    --   -- a≡b i ≡ y
+    --   -- ———— Boundary (wanted) —————————————————————————————————————
+    --   -- i = i0 ⊢ λ i₁ → Acontr y i₁
+    --   -- i = i1 ⊢ λ i₁ → Bcontr y i₁
 
-  -- z = let
-  --     z1 = λ (y : A≡B i) (j : I) →
-  --       let u = λ k → λ where
-  --         (i = i0) → Acontr y (~ j)
-  --         (i = i1) → Bcontr y j
-  --         (j = i0) → a≡b i
-  --         (j = i1) → {!  y i !}
-  --       in hfill u (inS (a≡b {! j  !})) j
-  --   in {!   !}
+    -- z = let
+    --     z1 = λ (y : A≡B i) (j : I) →
+    --       let u = λ k → λ where
+    --         (i = i0) → Acontr y (~ j)
+    --         (i = i1) → Bcontr y j
+    --         (j = i0) → a≡b i
+    --         (j = i1) → {!  y i !}
+    --       in hfill u (inS (a≡b {! j  !})) j
+    --   in {!   !}
 
 
 lemma (suc zero) (A , A-prop) (B , B-prop) x y i j = {!   !}
@@ -85,4 +105,4 @@ lemma (suc (suc n)) x y = {!   !}
 --     -- (glue (λ { (i = i1) → {!   !} }) {!   !})
 --     -- (glue (λ { (i = i0) → a ; (i = i1) → b }) b))
 -- lemma (suc n) x y = {!   !}
- 
\ No newline at end of file
+     
\ No newline at end of file