From ca5e41e464f773c82679e8343c922e002c8fbb9f Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Mon, 21 Oct 2024 02:34:42 -0500 Subject: [PATCH] give up on the corollary-equiv 3.5.1 for now --- src/CubicalHott/HLevels.agda | 40 +++++++ src/CubicalHott/Lemma3-5-1.agda | 35 +++++- src/CubicalHott/Theorem7-1-11.agda | 175 ++++++++++++++++++----------- src/CubicalHott/Theorem7-1-6.agda | 2 +- 4 files changed, 184 insertions(+), 68 deletions(-) create mode 100644 src/CubicalHott/HLevels.agda diff --git a/src/CubicalHott/HLevels.agda b/src/CubicalHott/HLevels.agda new file mode 100644 index 0000000..1cc7e90 --- /dev/null +++ b/src/CubicalHott/HLevels.agda @@ -0,0 +1,40 @@ +{-# OPTIONS --cubical #-} + +module CubicalHott.HLevels where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.HLevels +open import Cubical.Foundations.Structure +open import Data.Nat + +isOfHLevel' : ∀ {ℓ : Level} → ℕ → Type ℓ → Type ℓ +isOfHLevel' 0 A = isContr A +isOfHLevel' (suc n) A = (x y : A) → isOfHLevel' n (x ≡ y) + +TypeOfHLevel' : ∀ ℓ → HLevel → Type (ℓ-suc ℓ) +TypeOfHLevel' ℓ n = TypeWithStr ℓ (isOfHLevel' n) + +isOfHLevel→isOfHLevel' : ∀ {l : Level} → (n : ℕ) → (A : Type l) + → isOfHLevel n A → isOfHLevel' n A +isOfHLevel→isOfHLevel' zero A z = z +isOfHLevel→isOfHLevel' (suc zero) A z = + λ x y → (z x y) , λ q → isProp→isSet z x y (z x y) q +isOfHLevel→isOfHLevel' (suc (suc n)) A z = + λ x y p q → isOfHLevel→isOfHLevel' (suc n) (x ≡ y) (z x y) p q + +isOfHLevel'→isOfHLevel : ∀ {l : Level} → (n : ℕ) → (A : Type l) + → isOfHLevel' n A → isOfHLevel n A +isOfHLevel'→isOfHLevel zero A z = z +isOfHLevel'→isOfHLevel (suc zero) A z = + λ x y → let z1 = z x y in fst z1 +isOfHLevel'→isOfHLevel (suc (suc n)) A z = + λ x y → + let IHf = λ p q → z x y p q in + let IH = isOfHLevel'→isOfHLevel (suc n) (x ≡ y) IHf in + IH + +TypeOfHLevel→TypeOfHLevel' : ∀ (l : Level) → (n : ℕ) → TypeOfHLevel l n → TypeOfHLevel' l n +TypeOfHLevel→TypeOfHLevel' l n (T , T-n-type) = T , isOfHLevel→isOfHLevel' n T T-n-type + +TypeOfHLevel'→TypeOfHLevel : ∀ (l : Level) → (n : ℕ) → TypeOfHLevel' l n → TypeOfHLevel l n +TypeOfHLevel'→TypeOfHLevel l n (T , T-n-type) = T , isOfHLevel'→isOfHLevel n T T-n-type \ No newline at end of file diff --git a/src/CubicalHott/Lemma3-5-1.agda b/src/CubicalHott/Lemma3-5-1.agda index 0dc936e..784eb24 100644 --- a/src/CubicalHott/Lemma3-5-1.agda +++ b/src/CubicalHott/Lemma3-5-1.agda @@ -3,6 +3,9 @@ module CubicalHott.Lemma3-5-1 where open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Equiv +open import Cubical.Foundations.Isomorphism +open import Cubical.Data.Sigma lemma : {l l2 : Level} → {A : Type l} → {P : A → Type l2} → ((x : A) → isProp (P x)) @@ -12,4 +15,34 @@ lemma : {l l2 : Level} → {A : Type l} → {P : A → Type l2} 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 + +corollary : {l : Level} → {A B : Type l} + → (f g : A ≃ B) + → fst f ≡ fst g + → f ≡ g +corollary f g p = lemma isPropIsEquiv f g p + +corollary-equiv : {l : Level} → {A B : Type l} + → (f g : A ≃ B) + → (fst f ≡ fst g) ≃ (f ≡ g) +corollary-equiv f g = isoToEquiv (iso (corollary f g) (cong fst) fg gf) where + helper : (f≡g : f ≡ g) → subst (λ x → isEquiv (fst x)) f≡g (snd f) ≡ snd g + helper f≡g = isPropIsEquiv (fst g) (subst (λ x → isEquiv (fst x)) f≡g (snd f)) (snd g) + + helper2 : (f≡g : f ≡ g) → PathP (λ i → isEquiv (fst (f≡g i))) (snd f) (snd g) + helper2 f≡g = toPathP (helper f≡g) + + fg : section (corollary f g) (cong fst) + -- Trying to prove that producing full f ≡ g after discarding the second half still produces the original + -- However, no matter what the original is, the isEquiv part is a mere prop + fg f≡g i j = fst (f≡g j) , {! !} where + -- isEquiv (fst (f≡g j)) + -- ———— Boundary (wanted) ————————————————————————————————————— + -- j = i0 ⊢ f .snd + -- j = i1 ⊢ g .snd + -- i = i0 ⊢ CubicalHott.Lemma3-5-1.goal isPropIsEquiv f g + -- (cong (λ r → fst r) f≡g) j j + -- i = i1 ⊢ f≡g j .snd + + gf : retract (corollary f g) (cong fst) + gf x = refl diff --git a/src/CubicalHott/Theorem7-1-11.agda b/src/CubicalHott/Theorem7-1-11.agda index e6cbac1..8e99cf2 100644 --- a/src/CubicalHott/Theorem7-1-11.agda +++ b/src/CubicalHott/Theorem7-1-11.agda @@ -11,67 +11,97 @@ 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.Lemma3-5-1 renaming (lemma to lemma3-5-1; corollary to corollary3-5-1) +open import CubicalHott.Theorem7-1-6 renaming (theorem to theorem7-1-6) open import CubicalHott.Theorem7-1-8 renaming (theorem to theorem7-1-8) open import CubicalHott.Theorem7-1-10 renaming (theorem to theorem7-1-10) +open import CubicalHott.HLevels -lemma : ∀ {l} → (n : HLevel) → isOfHLevel (suc n) (TypeOfHLevel l n) -lemma zero (A , a , Acontr) (B , b , Bcontr) i = - A≡B i , goal i where - -- isContr (A≡B i) - -- Acontr ≡ Bcontr - - -- A≡B i , a≡b i , λ y j → wtf i y j where +helper : ∀ {l} → (n : HLevel) → isOfHLevel' (suc n) (TypeOfHLevel l n) +helper zero TA @ (A , a , Acontr) TB @ (B , b , Bcontr) = + (λ i → A≡B i , goal2 i) , goal6 where eqv1 : A ≃ B eqv1 = isoToEquiv (iso (λ _ → b) (λ _ → a) Bcontr Acontr) - A≡B : A ≡ B A≡B = ua eqv1 - a≡b : PathP (λ i → A≡B i) a b a≡b j = glue (λ { (j = i0) → a ; (j = i1) → b }) b - 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)) + goal2 : PathP (λ i → isContr (A≡B i)) (a , Acontr) (b , Bcontr) + goal3 : subst isContr A≡B (a , Acontr) ≡ (b , Bcontr) + goal2 = toPathP goal3 + goal4 : (x : B) → isProp ((y : B) → x ≡ y) + goal3 = lemma3-5-1 goal4 (subst isContr A≡B (a , Acontr)) (b , Bcontr) (fromPathP a≡b) + goal5 : isSet B + goal4 x f1 f2 = funExt λ (y : B) → goal5 x y (f1 y) (f2 y) + goal5 = isProp→isSet (isContr→isProp (b , Bcontr)) - 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) + goal6 : (q : TA ≡ TB) → (λ i → A≡B i , goal2 i) ≡ q + goal6 q = {! !} - goal : PathP (λ i → isContr (A≡B i)) (a , Acontr) (b , Bcontr) - goal = toPathP helper + -- A≡B i , goal i where + -- -- isContr (A≡B i) + -- -- Acontr ≡ Bcontr - -- -- eqv2 : ((y : A) → a ≡ y) ≡ ((y : B) → b ≡ y) - -- -- eqv2 = λ i → (y : A≡B i) → a≡b i ≡ y + -- -- A≡B i , a≡b i , λ y j → wtf i y j where + -- eqv1 : A ≃ B + -- eqv1 = isoToEquiv (iso (λ _ → b) (λ _ → a) Bcontr Acontr) - -- -- 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 + -- A≡B : A ≡ B + -- A≡B = ua eqv1 + + -- a≡b : PathP (λ i → A≡B i) a b + -- a≡b j = glue (λ { (j = i0) → a ; (j = i1) → b }) b + + -- helper3 : (x : B) → isProp ((y : B) → x ≡ y) + -- helper3 x f1 f2 = + -- let helper = isProp→isSet (isContr→isProp (b , Bcontr)) in + -- funExt (λ (y : B) → helper x y (f1 y) (f2 y)) + + -- helper2 : subst isContr A≡B (a , Acontr) ≡ (b , Bcontr) + -- helper2 = lemma3-5-1 helper3 (subst isContr A≡B (a , Acontr)) (b , Bcontr) (fromPathP a≡b) + + -- goal : PathP (λ i → isContr (A≡B i)) (a , Acontr) (b , Bcontr) + -- goal = toPathP helper2 + +helper {l = l} (suc n) (X , px) (Y , py) p q = {! !} where + goal1 : ((X , px) ≡ (Y , py)) ≃ (X ≃ Y) + goal1 = let z = pathToEquiv {! !} in {! !} + + +lemma : ∀ {l} → (n : HLevel) → isOfHLevel (suc n) (TypeOfHLevel l n) +lemma {l = l} n = isOfHLevel'→isOfHLevel (suc n) (TypeOfHLevel l n) (helper n) + +-- -- -- 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 !} +-- -- -- 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) +-- -- 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 → {! !} +-- -- 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 {l = l} (suc zero) (A , A-prop) (B , B-prop) p q i j = {! !} , {! !} where z1 = let z = lemma {l = l} zero in {! !} @@ -81,35 +111,48 @@ lemma {l = l} (suc zero) (A , A-prop) (B , B-prop) p q i j = {! !} , {! !} w -- cong_fst(p) : A ≡ B -lemma (suc (suc n)) x y p q = - let IH = lemma (suc n) in - {! !} +-- -- we know that A ≡ B in two different ways +-- -- if A is a prop, then (x y : A) → x ≡ y +-- -- if A is empty, then B is also empty +-- -- but we can't choose a contractible center (no AOC) + +-- -- "for any two proofs that A ≡ B and that A-prop ≡ B-prop" +-- -- p : (A , A-prop) ≡ (B , B-prop) +-- -- p = λ i → +-- -- so (p i0) : Σ Type isProp = (A , A-prop) +-- -- p ≡_{Σ Type isProp} q +-- -- through lemma 3.5.1, if the isProp is a prop for every type, then we only have to compare the Type +-- -- +-- {! !} --- lemma : ∀ {l} → (n : HLevel) → isOfHLevel (suc n) (TypeOfHLevel l n) --- lemma zero (A , a , Acontr) (B , b , Bcontr) i = G , g , contr where +-- lemma (suc (suc n)) x y p q = +-- let IH = lemma (suc n) in +-- {! !} --- eqv1 : A ≃ B --- eqv1 = isoToEquiv (iso (λ _ → b) (λ _ → a) Bcontr Acontr) +-- -- lemma : ∀ {l} → (n : HLevel) → isOfHLevel (suc n) (TypeOfHLevel l n) +-- -- lemma zero (A , a , Acontr) (B , b , Bcontr) i = G , g , contr where --- T = λ { (i = i0) → A ; (i = i1) → B } --- e = λ { (i = i0) → eqv1 ; (i = i1) → idEquiv B } +-- -- eqv1 : A ≃ B +-- -- eqv1 = isoToEquiv (iso (λ _ → b) (λ _ → a) Bcontr Acontr) --- G = primGlue B T e --- g = glue {T = T} {e = e} (λ { (i = i0) → a ; (i = i1) → b }) b +-- -- T = λ { (i = i0) → A ; (i = i1) → B } +-- -- e = λ { (i = i0) → eqv1 ; (i = i1) → idEquiv B } --- -- at i = i0, y = a --- -- at i = i1, y = b +-- -- G = primGlue B T e +-- -- g = glue {T = T} {e = e} (λ { (i = i0) → a ; (i = i1) → b }) b --- -- For some arbitrary y : G, prove g ≡ y --- contr : (y : G) → g ≡ y --- contr y j = {! !} --- -- let p = λ where --- -- (i = i0) → {! !} -- Acontr (unglue {A = A} (~ i) {T = T} {e = λ { (i = i0) → idEquiv A }} y) j --- -- (i = i1) → Bcontr (unglue {A = B} i {T = T} {e = λ { (i = i1) → idEquiv B }} y) j --- -- in glue p (Bcontr {! g !} {! j !}) +-- -- -- at i = i0, y = a +-- -- -- at i = i1, y = b --- -- unglue i {! !} --- -- (glue (λ { (i = i1) → {! !} }) {! !}) --- -- (glue (λ { (i = i0) → a ; (i = i1) → b }) b)) --- lemma (suc n) x y = {! !} - \ No newline at end of file +-- -- -- For some arbitrary y : G, prove g ≡ y +-- -- contr : (y : G) → g ≡ y +-- -- contr y j = {! !} +-- -- -- let p = λ where +-- -- -- (i = i0) → {! !} -- Acontr (unglue {A = A} (~ i) {T = T} {e = λ { (i = i0) → idEquiv A }} y) j +-- -- -- (i = i1) → Bcontr (unglue {A = B} i {T = T} {e = λ { (i = i1) → idEquiv B }} y) j +-- -- -- in glue p (Bcontr {! g !} {! j !}) + +-- -- -- unglue i {! !} +-- -- -- (glue (λ { (i = i1) → {! !} }) {! !}) +-- -- -- (glue (λ { (i = i0) → a ; (i = i1) → b }) b)) +-- -- lemma (suc n) x y = {! !} diff --git a/src/CubicalHott/Theorem7-1-6.agda b/src/CubicalHott/Theorem7-1-6.agda index 7f53c93..c9cab8d 100644 --- a/src/CubicalHott/Theorem7-1-6.agda +++ b/src/CubicalHott/Theorem7-1-6.agda @@ -9,7 +9,7 @@ open import Cubical.Foundations.HLevels open import Cubical.Functions.Embedding open import Data.Nat -theorem : {X Y : Type} +theorem : {l : Level} → {X Y : Type l} → (f : X → Y) → isEmbedding f → (n : HLevel) → isOfHLevel (suc n) Y → isOfHLevel (suc n) X