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-11-01 12:58:35 -05:00
parent d17901e7d6
commit 604a5045c4
12 changed files with 100 additions and 64 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/CubicalHott/Corollary7-1-5.agda
View file

@ -10,7 +10,7 @@ open import Cubical.Data.Nat
open import CubicalHott.Theorem7-1-4 renaming (theorem to theorem7-1-4)
corollary : {X Y : Type} → (n : ℕ)
corollary : {l : Level} → {X Y : Type l} → (n : ℕ)
→ X ≃ Y → isOfHLevel n X → isOfHLevel n Y
corollary n eqv prf =
theorem7-1-4 (fst eqv) (invIsEq (snd eqv))

14
src/CubicalHott/Corollary7-2-3.agda Normal file
View file

@ -0,0 +1,14 @@
{-# OPTIONS --cubical #-}
module CubicalHott.Corollary7-2-3 where
open import Cubical.Foundations.Prelude
open import Cubical.Relation.Nullary
open import CubicalHott.Lemma7-2-4 renaming (lemma to lemma7-2-4)
corollary : {X : Type}
→ ((x y : X) → ¬ ¬ (x ≡ y) → x ≡ y)
→ isSet X
corollary {X} prf x y p q = {! !} where
wtf = let z = prf x y (λ r → r p) in {! !}

2
src/CubicalHott/HLevels.agda
View file

@ -14,7 +14,7 @@ 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 : {l : Level} → (T : Type l) → 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

2
src/CubicalHott/Lemma2-4-3.agda
View file

@ -6,7 +6,7 @@ open import Cubical.Foundations.Prelude
open import Cubical.Homotopy.Base
postulate
lemma : {A B : Type} → (f g : A → B) → (H : f ∼ g) → {x y : A} → (p : x ≡ y)
lemma : {l : Level} → {A B : Type l} → (f g : A → B) → (H : f ∼ g) → {x y : A} → (p : x ≡ y)
→ H x ∙ cong g p ≡ cong f p ∙ H y
-- lemma f g H {x} {y} p i j =
-- -- B

13
src/CubicalHott/Lemma7-2-4.agda Normal file
View file

@ -0,0 +1,13 @@
{-# OPTIONS --cubical #-}
module CubicalHott.Lemma7-2-4 where
open import Cubical.Foundations.Prelude
open import Cubical.Relation.Nullary
open import Cubical.Data.Sigma
open import Cubical.Data.Empty
open import Data.Sum
lemma : (A : Type) → (A ⊎ ¬ A) → (¬ ¬ A → A)
lemma A (inj₁ x) p = x
lemma A (inj₂ y) p = elim (p y)

2
src/CubicalHott/Theorem2-7-2.agda
View file

@ -7,7 +7,7 @@ open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Data.Sigma
theorem : {A : Type} {P : A → Type} {w w' : Σ A P}
theorem : {l l2 : Level} → {A : Type l} → {P : A → Type l2} → {w w' : Σ A P}
→ (w ≡ w') ≃ Σ (fst w ≡ fst w') (λ p → PathP (λ i → P (p i)) (snd w) (snd w'))
theorem {P = P} {w = w} {w' = w'} =
isoToEquiv (iso f g fg gf) where

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

@ -2,6 +2,7 @@
module CubicalHott.Theorem7-1-11 where
open import Agda.Primitive using (lzero ; lsuc)
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Core.Glue
@ -19,35 +20,7 @@ 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 : ∀ {l : Level} → (n : HLevel) → isOfHLevel' {ℓ = lsuc l} (suc n) (TypeOfHLevel l n)
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))))
@ -58,7 +31,32 @@ helper {l = l} zero = goal1 where
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
-- 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
helper {l = l} (suc n) (X , px) (Y , py) p q = isOfHLevel→isOfHLevel' n (p ≡ q) goal4 where
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) =
@ -71,15 +69,18 @@ helper {l = l} (suc n) (X , px) (Y , py) p q = {! !} where
g : X ≡ Y → (X , px) ≡ (Y , py)
g p = lemma3-5-1 (λ x → theorem7-1-10 n) (X , px) (Y , py) p
,snd, : (p : (X , px) ≡ (Y , py)) → PathP {ℓ = l} (λ i → isOfHLevel n (cong fst p i)) px py
,snd, p = J (λ y' p' → PathP (λ i → isOfHLevel n (cong fst p' i)) px (snd y')) refl 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
gf p i j = {! goal i j !} where
goal : SquareP (λ i j → isOfHLevel {ℓ = lsuc l} n (cong {! !} p i)) refl refl {! g (f p) !} λ i → {! snd (p i) !}
prop-helper : isProp (isOfHLevel n Y)
prop-helper = theorem7-1-10 n
thm : transport {ℓ = l} (λ i → isOfHLevel {ℓ = l} n (fst (p i))) px ≡ py
thm = prop-helper (transport (λ i → isOfHLevel n (fst (p i))) px) py
goal2 : isEmbedding {A = X ≃ Y} {B = X → Y} fst
goal2 x≃y1 x≃y2 = isoToIsEquiv (iso (cong fst) g (λ _ → refl) gf) where
@ -106,10 +107,13 @@ helper {l = l} (suc n) (X , px) (Y , py) p q = {! !} where
goal3 = theorem7-1-6 {! !} goal2 {! suc n !} {! !} {! !}
goal4 : isOfHLevel n (p ≡ q)
goal4 = {! !}
goal4 =
let IH = helper n in
isOfHLevel'→isOfHLevel n {! !} {! IH p q !}
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
@ -195,4 +199,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 = {! !}

8
src/CubicalHott/Theorem7-1-4.agda
View file

@ -12,21 +12,21 @@ open import Cubical.Data.Nat
open import CubicalHott.Lemma2-4-3 renaming (lemma to lemma2-4-3)
theorem : {X Y : Type}
theorem : {l : Level} → {X Y : Type l}
→ (p : X → Y)
→ (s : Y → X)
→ retract s p
→ (n : ℕ)
→ isOfHLevel n X
→ isOfHLevel n Y
theorem {X} {Y} p s r zero (x0 , xContr) = p x0 , λ y → cong p (xContr (s y)) ∙ r y
theorem {X} {Y} p s r (suc zero) xHlevel a b =
theorem {X = X} {Y = Y} p s r zero (x0 , xContr) = p x0 , λ y → cong p (xContr (s y)) ∙ r y
theorem {X = X} {Y = Y} p s r (suc zero) xHlevel a b =
let
step1 = xHlevel (s a) (s b)
step2 = cong p step1
step3 = (sym (r a)) ∙ step2 ∙ r b
in step3
theorem {X} {Y} p s r (suc (suc n)) xHlevel a b =
theorem {X = X} {Y = Y} p s r (suc (suc n)) xHlevel a b =
theorem (λ q → sym (r a) ∙ cong p q ∙ r b) (cong s) f (suc n) (xHlevel (s a) (s b)) where
f : retract (cong s) (λ q → sym (r a) ∙ cong p q ∙ r b)
f q = cong (sym (r a) ∙_) helper ∙ assoc (sym (r a)) (r a) q ∙ cong (_∙ q) (lCancel (r a)) ∙ sym (lUnit q) where

8
src/CubicalHott/Theorem7-1-7.agda
View file

@ -6,17 +6,17 @@ open import Data.Nat
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
theorem : {X : Type} {n : ℕ}
theorem : {l : Level} → {X : Type l} → {n : ℕ}
→ isOfHLevel n X → isOfHLevel (suc n) X
theorem {X} {zero} X-n-type x y = sym (snd X-n-type x) ∙ snd X-n-type y
theorem {X} {suc zero} X-n-type x y p q j i =
theorem {X = X} {n = zero} X-n-type x y = sym (snd X-n-type x) ∙ snd X-n-type y
theorem {X = X} {n = suc zero} X-n-type x y p q j i =
let u = λ k → λ where
(i = i0) → X-n-type x x k
(i = i1) → X-n-type x y k
(j = i0) → X-n-type x (p i) k
(j = i1) → X-n-type x (q i) k
in hcomp u x
theorem {X} {2+ n} X-n-type = λ x y p q →
theorem {X = X} {n = 2+ n} X-n-type = λ x y p q →
let known = X-n-type x y in
let IH = theorem {X = x ≡ y} {n = suc n} known p q in
IH

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

@ -12,11 +12,11 @@ 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 : ℕ}
theorem : {l l2 : Level} → {A : Type l} → {B : A → Type l2} → {n : ℕ}
→ isOfHLevel n A
→ ((a : A) → isOfHLevel n (B a))
→ isOfHLevel n (Σ A B)
theorem {A} {B} {zero} A-n-type @ (a , a-contr) B-n-type =
theorem {A = A} {B} {zero} A-n-type @ (a , a-contr) B-n-type =
let b = fst (B-n-type a) in
let b-contr = snd (B-n-type a) in
(a , b) , λ y i → a-contr (fst y) i ,
@ -25,11 +25,11 @@ theorem {A} {B} {zero} A-n-type @ (a , a-contr) B-n-type =
-- using path induction, both of them are a
let helper = J (λ a' p' → (b' : B a') → PathP (λ i → B (p' i)) b b') (λ b' j → b-contr b' j ) (a-contr (fst y)) (snd y) in
helper i
theorem {A} {B} {suc zero} A-n-type B-n-type x @ (xa , xb) y @ (ya , yb) =
theorem {A = A} {B} {suc zero} A-n-type B-n-type x @ (xa , xb) y @ (ya , yb) =
λ i → A-n-type xa ya i ,
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) =
theorem {A = A} {B} {2+ n} A-n-type B-n-type x @ (xa , xb) y @ (ya , yb) =
let eqv = theorem2-7-2 {w = x} {w' = y} in
let eqv2 = (fst invEquivEquiv) eqv in
let

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

@ -8,7 +8,7 @@ open import Cubical.Foundations.Equiv
open import Cubical.Functions.FunExtEquiv
open import Data.Nat
theorem : {A : Type} {B : A → Type}
theorem : {l l2 : Level} → {A : Type l} {B : A → Type l2}
→ (n : ℕ)
→ ((a : A) → isOfHLevel n (B a))
→ isOfHLevel n ((x : A) → B x)

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

@ -2,14 +2,19 @@
module CubicalHott.Theorem7-2-2 where
open import Agda.Primitive hiding (Prop)
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Structure
open import Cubical.Data.Sigma
theorem : {X : Type}
→ (R : X → X → Type)
→ ((x : X) → R x x → x ≡ x)
→ ((x y : X) → (R x y) → x ≡ y)
Prop : (l : Level) → Type (lsuc l)
Prop l = TypeWithStr l isProp
theorem : {l l2 : Level} → {X : Type l}
→ (R : X → X → Prop l2)
→ ((x : X) → {! R x x !} → {! !})
→ ((x y : X) → {! R x y !} → x ≡ y)
→ isSet X
theorem R f1 f2 x y p q =
{! !}
theorem R f1 f2 x y p q = {! !}