give up on the corollary-equiv 3.5.1 for now

This commit is contained in:
Michael Zhang 2024-10-21 02:34:42 -05:00
parent 26ea102563
commit ca5e41e464
4 changed files with 184 additions and 68 deletions

View file

@ -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

View file

@ -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))
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

View file

@ -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 → <something s.t at i=0, returns A , A-prop>
-- -- 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 = {! !}
-- -- -- 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 = {! !}

View file

@ -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