michael/type-theory
2
0
Fork 0
Code Issues 21 Pull requests Projects 1 Releases 1 Packages Wiki Activity Actions

wip

Browse source
This commit is contained in:
Michael Zhang 2024-10-23 10:42:13 -05:00
parent ca5e41e464
commit d17901e7d6
7 changed files with 123 additions and 167 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/CubicalHott/HLevels.agda
View file

@ -14,6 +14,12 @@ isOfHLevel' (suc n) A = (x y : A) → isOfHLevel' n (x ≡ y)
TypeOfHLevel' : ∀ ℓ → HLevel → Type (ℓ-suc ℓ)
TypeOfHLevel' ℓ n = TypeWithStr ℓ (isOfHLevel' n)
1Prop : (T : Type) → isOfHLevel' 1 T → isProp T
1Prop T T1 x y = let z = T1 x y in fst z
Prop1 : {l : Level} → (T : Type l) → isProp T → isOfHLevel' 1 T
Prop1 T Tp x y = (Tp x y) , λ q → isProp→isSet Tp x y (Tp x y) q
isOfHLevel→isOfHLevel' : ∀ {l : Level} → (n : ℕ) → (A : Type l)
→ isOfHLevel n A → isOfHLevel' n A
isOfHLevel→isOfHLevel' zero A z = z

42
src/CubicalHott/Lemma3-5-1.agda
View file

@ -22,27 +22,27 @@ corollary : {l : Level} → {A B : Type l}
→ 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)
-- 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)
-- 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
-- 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
-- gf : retract (corollary f g) (cong fst)
-- gf x = refl

11
src/CubicalHott/Lemma8-3-1.agda
View file

@ -14,12 +14,13 @@ open import Cubical.Homotopy.Loopspace
open import Cubical.HITs.SetTruncation
helper : ∀ {l : Level} → (n : ℕ) → (A∙ @ (A , a) : Pointed l)
helper : ∀ {l : Level} → (n : ℕ)
→ (A∙ @ (A , a) : Pointed l)
→ isOfHLevel (suc n) A → isOfHLevel n (typ (Ω A∙))
helper zero A∙@(A , a) prf = refl , (λ y j i → {! !})
helper zero A∙@(A , a) prf = refl , {! !}
helper (suc zero) A∙@(A , a) prf = {! !}
helper (suc (suc n)) A∙@(A , a) prf = {! !}
-- lemma : ∀ {l} → (A∙ @ (A , a) : Pointed l)
-- → (n : ℕ) → hLevelTrunc n A → (k : ℕ) → π (k + n) (A , a) ≡ Lift Unit
-- lemma A∙ @ (A , a) n x k i = {! !} where
lemma : ∀ {l} → (A∙ @ (A , a) : Pointed l)
→ (n : ℕ) → hLevelTrunc n A → (k : ℕ) → π (k + n) (A , a) ≡ Lift Unit
lemma A∙ @ (A , a) n x k = {! !}

134
src/CubicalHott/Theorem7-1-11.agda
View file

@ -7,6 +7,8 @@ open import Cubical.Foundations.HLevels
open import Cubical.Core.Glue
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Data.Sigma
open import Cubical.Functions.Embedding
open import Cubical.Foundations.Univalence
open import Cubical.Data.Nat
open import Data.Unit
@ -17,60 +19,97 @@ 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 {l = l} zero = goal2 where
eqv : (x y : TypeOfHLevel l zero) → fst x ≡ fst y
eqv x y = ua (isoToEquiv (iso (λ _ → fst (snd y)) (λ _ → fst (snd x)) (snd (snd y)) (snd (snd x))))
goal2 : isProp (TypeOfHLevel l zero)
goal2 x y = lemma3-5-1 (λ _ → theorem7-1-10 zero) x y (eqv x y)
lemma {l = l} (suc zero) x @ (X , Xprop) y @ (Y , Yprop) = goal1 where
IH : isProp (TypeOfHLevel l 0)
IH = lemma zero
goal1 : isProp (x ≡ y)
goal1 p q = {! !}
lemma {l = l} (suc (suc n)) x @ (X , px) y @ (Y , py) p q = {! !} where
IH : isOfHLevel (suc (suc n)) (TypeOfHLevel l (suc n))
IH = lemma (suc n)
goal2 : isEmbedding {A = X ≃ Y} {B = X → Y} fst
goal2 x≃y1 x≃y2 = isoToIsEquiv (iso (cong fst) g (λ _ → refl) gf) where
g : fst x≃y1 ≡ fst x≃y2 → x≃y1 ≡ x≃y2
g = lemma3-5-1 isPropIsEquiv x≃y1 x≃y2
gf : retract (cong fst) g
gf p i j = fst (p j) , {! !}
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
helper {l = l} zero = goal1 where
eqv : (x y : TypeOfHLevel l zero) → fst x ≡ fst y
eqv x y = ua (isoToEquiv (iso (λ _ → fst (snd y)) (λ _ → fst (snd x)) (snd (snd y)) (snd (snd x))))
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))
goal2 : isProp (TypeOfHLevel l zero)
goal2 x y = lemma3-5-1 (λ _ → theorem7-1-10 zero) x y (eqv x y)
goal6 : (q : TA ≡ TB) → (λ i → A≡B i , goal2 i) ≡ q
goal6 q = {! !}
-- 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
-- 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
-- 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
goal1 : (x y : TypeOfHLevel l zero) → isContr (x ≡ y)
goal1 = Prop1 (TypeOfHLevel l zero) goal2
helper {l = l} (suc n) (X , px) (Y , py) p q = {! !} where
goal1 : ((X , px) ≡ (Y , py)) ≃ (X ≃ Y)
goal1 = let z = pathToEquiv {! !} in {! !}
goal1 : {n : ℕ} → ((X , px) : TypeOfHLevel l n) → ((Y , py) : TypeOfHLevel l n)
→ ((X , px) ≡ (Y , py)) ≃ (X ≃ Y)
goal1 {n = n} (X , px) (Y , py) =
(X , px) ≡ (Y , py) ≃⟨ isoToEquiv (iso f g (λ _ → refl) gf) ⟩
X ≡ Y ≃⟨ univalence ⟩
X ≃ Y ■ where
f : (X , px) ≡ (Y , py) → X ≡ Y
f = cong fst
g : X ≡ Y → (X , px) ≡ (Y , py)
g p = lemma3-5-1 (λ x → theorem7-1-10 n) (X , px) (Y , py) p
gf : retract f g
gf p i j = fst (p j) , {! !}
where
wtf =
let z1 = helper n (X , px) (Y , py) in
let z2 = isOfHLevel'→isOfHLevel n ((X , px) ≡ (Y , py)) z1 in
{! !}
prop-helper : isProp (isOfHLevel n Y)
prop-helper = theorem7-1-10 n
goal2 : isEmbedding {A = X ≃ Y} {B = X → Y} fst
goal2 x≃y1 x≃y2 = isoToIsEquiv (iso (cong fst) g (λ _ → refl) gf) where
g : fst x≃y1 ≡ fst x≃y2 → x≃y1 ≡ x≃y2
g = lemma3-5-1 isPropIsEquiv x≃y1 x≃y2
gf : retract (cong fst) g
gf p i j = fst (p j) , {! !}
-- Goal here is to use toPathP, convert them both
-- isEquiv (fst (p j))
-- ———— Boundary (wanted) —————————————————————————————————————
-- j = i0 ⊢ x≃y1 .snd
-- j = i1 ⊢ x≃y2 .snd
-- i = i0 ⊢ CubicalHott.Lemma3-5-1.goal isPropIsEquiv x≃y1 x≃y2
-- (cong (λ r → fst r) p) j j
-- i = i1 ⊢ p j .snd
-- toPathP {A = {! !}} z j where
-- z : transport (λ i → isEquiv (fst (p i))) (snd x≃y1) ≡ snd x≃y2
-- z = isPropIsEquiv (fst x≃y2) (subst (λ x → isEquiv (fst x)) p (snd x≃y1)) (snd x≃y2)
goal3 : isOfHLevel n (X → Y)
goal3 = theorem7-1-6 {! !} goal2 {! suc n !} {! !} {! !}
goal4 : isOfHLevel n (p ≡ q)
goal4 = {! !}
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
@ -156,3 +195,4 @@ lemma {l = l} (suc zero) (A , A-prop) (B , B-prop) p q i j = {! !} , {! !} w
-- -- -- (glue (λ { (i = i1) → {! !} }) {! !})
-- -- -- (glue (λ { (i = i0) → a ; (i = i1) → b }) b))
-- -- lemma (suc n) x y = {! !}

1
src/CubicalHott/Theorem7-1-9.agda
View file

@ -22,6 +22,7 @@ theorem (suc zero) prf f1 f2 i x =
result i
theorem {A = A} {B = B} (2+ n) prf f1 f2 =
subst (isOfHLevel (suc n)) funExtPath (theorem (suc n) λ a → prf a (f1 a) (f2 a))
-- goal1 where
-- goal1 : isOfHLevel (suc n) (f1 ≡ f2)
-- goal2 : isOfHLevel (suc n) ((a : A) → f1 a ≡ f2 a)

3
src/CubicalHott/Theorem7-2-2.agda
View file

@ -11,4 +11,5 @@ theorem : {X : Type}
→ ((x : X) → R x x → x ≡ x)
→ ((x y : X) → (R x y) → x ≡ y)
→ isSet X
theorem R r f x y p q = {! !}
theorem R f1 f2 x y p q =
{! !}

93
src/ThesisWork/LES.agda
View file

@ -1,93 +0,0 @@
{-# OPTIONS --cubical #-}
module ThesisWork.LES where
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.Equiv
open import Data.Nat
open import Data.Fin
open import Data.Product
open import Cubical.Homotopy.Base
open import Cubical.Homotopy.Loopspace
open import Cubical.Homotopy.Group.Base
open import Cubical.Homotopy.Group.LES
open import Cubical.HITs.SetTruncation renaming (map to mapTrunc)
open import Cubical.HITs.SetTruncation.Fibers
private
variable
X Y : Type
LES-node : ∀ {l} → {X Y : Pointed l} → (f : X →∙ Y) → ℕ × Fin 3 → Type l
LES-node {Y = Y} f (n , zero) = π n Y
LES-node {X = X} f (n , suc zero) = π n X
LES-node {X = (X , x)} {Y = (Y , y)} (f , f-eq) (n , suc (suc zero)) =
let F = fiber f y in
π n (F , x , f-eq)
sucF : ℕ × Fin 3 → ℕ × Fin 3
sucF (n , zero) = n , suc zero
sucF (n , suc zero) = n , suc (suc zero)
sucF (n , suc (suc zero)) = suc n , zero
LES-edge : ∀ {l} → {X∙ Y∙ : Pointed l} → (f∙ : X∙ →∙ Y∙) → (n : ℕ × Fin 3)
→ LES-node f∙ (sucF n) → LES-node f∙ n
LES-edge {X∙ = X∙ @ (X , x)} {Y∙ = Y∙ @ (Y , y)} f∙ @ (f , f-eq) (n , zero) = h n where
h1 : ∀ (n : ℕ) → (Ω^ n) X∙ →∙ (Ω^ n) Y∙
h1 zero = f∙
h1 (suc n) = (λ x → refl) , helper where
helper : refl ≡ snd (Ω ((Ω^ n) Y∙))
helper i j = (Ω^ n) (Y , y) .snd
-- helper = λ i j →
-- let
-- top : (Ω^ n) (Y , y) .fst
-- top = {! refl !}
-- u = λ k → λ where
-- (i = i0) → {! !}
-- (i = i1) → {! !}
-- (j = i0) → {! !}
-- (j = i1) → {! !}
-- in hcomp u {! !}
h : ∀ (n : ℕ) → π n X∙ → π n Y∙
h n = mapTrunc (fst (h1 n))
-- h zero ∣ a ∣₂ = ∣ f a ∣₂
-- h (suc n) ∣ a ∣₂ = let IH = h n ∣ a i0 ∣₂ in ∣ {! !} ∣₂
-- h zero (squash₂ a b p q i j) = squash₂ (h 0 a) (h 0 b) (cong (h 0) p) (cong (h 0) q) i j
-- h (suc n) (squash₂ a b p q i j) = {! !}
LES-edge {X∙ = X∙ @ (X , x)} {Y∙ = Y∙ @ (Y , y)} f∙ @ (f , f-eq) (n , suc zero) = h n where
F = fiber f y
h1 : ∀ (n : ℕ) → (Ω^ n) (F , x , f-eq) →∙ (Ω^ n) X∙
h1 zero = fst , refl
h1 (suc n) = (λ f i → (Ω^ n) (X , x) .snd) , λ i j → (Ω^ n) (X , x) .snd
h : ∀ (n : ℕ) → π n (F , x , f-eq) → π n X∙
h n = mapTrunc (fst (h1 n))
LES-edge {X∙ = X∙ @ (X , x)} {Y∙ = Y∙ @ (Y , y)} f∙ @ (f , f-eq) (n , suc (suc zero)) = h n where
F = fiber f y
h1 : ∀ (n : ℕ) → (Ω^ (suc n)) Y∙ →∙ (Ω^ n) (F , x , f-eq)
h1 zero = (λ y → x , f-eq) , refl
h1 (suc n) = (λ y i → (Ω^ n) (F , x , f-eq) .snd) , λ i j → (Ω^ n) (F , x , f-eq) .snd
h : ∀ (n : ℕ) → π (suc n) Y∙ → π n (F , x , f-eq)
h n = mapTrunc (fst (h1 n))
-- LES-edge f n_ with mapN n_
-- LES-edge {X = X∙ @ (X , x)} {Y = Y∙ @ (Y , y)} f n_ | (n , zero) = {! h !} where
-- h : π n X∙ → π n Y∙
-- h ∣ x ∣₂ = ∣ {! !} ∣₂
-- h (squash₂ z z₁ p q i i₁) = {! !}
-- -- z : LES-node f (mapN (suc n_))
-- -- z : π n X
-- -- z : ∥ typ ((Ω^ 0) X) ∥₂
-- -- z : ∥ typ X ∥₂
-- -- z : ∥ typ X ∥₂
-- LES-edge f n_ | (n , suc zero) = λ z → {! !}
-- LES-edge f n_ | (n , suc (suc zero)) = λ z → {! !}