From 604a5045c4769c4dad3e1f96c5bd2a0edd5b57ce Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Fri, 1 Nov 2024 12:58:35 -0500 Subject: [PATCH] wip --- src/CubicalHott/Corollary7-1-5.agda | 2 +- src/CubicalHott/Corollary7-2-3.agda | 14 +++++ src/CubicalHott/HLevels.agda | 2 +- src/CubicalHott/Lemma2-4-3.agda | 2 +- src/CubicalHott/Lemma7-2-4.agda | 13 +++++ src/CubicalHott/Theorem2-7-2.agda | 2 +- src/CubicalHott/Theorem7-1-11.agda | 86 +++++++++++++++-------------- src/CubicalHott/Theorem7-1-4.agda | 8 +-- src/CubicalHott/Theorem7-1-7.agda | 8 +-- src/CubicalHott/Theorem7-1-8.agda | 8 +-- src/CubicalHott/Theorem7-1-9.agda | 2 +- src/CubicalHott/Theorem7-2-2.agda | 17 ++++-- 12 files changed, 100 insertions(+), 64 deletions(-) create mode 100644 src/CubicalHott/Corollary7-2-3.agda create mode 100644 src/CubicalHott/Lemma7-2-4.agda diff --git a/src/CubicalHott/Corollary7-1-5.agda b/src/CubicalHott/Corollary7-1-5.agda index 32a9d00..d691104 100644 --- a/src/CubicalHott/Corollary7-1-5.agda +++ b/src/CubicalHott/Corollary7-1-5.agda @@ -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)) diff --git a/src/CubicalHott/Corollary7-2-3.agda b/src/CubicalHott/Corollary7-2-3.agda new file mode 100644 index 0000000..52d1b79 --- /dev/null +++ b/src/CubicalHott/Corollary7-2-3.agda @@ -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 {! !} diff --git a/src/CubicalHott/HLevels.agda b/src/CubicalHott/HLevels.agda index ce118fb..41d6bd6 100644 --- a/src/CubicalHott/HLevels.agda +++ b/src/CubicalHott/HLevels.agda @@ -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 diff --git a/src/CubicalHott/Lemma2-4-3.agda b/src/CubicalHott/Lemma2-4-3.agda index 39844b0..be98343 100644 --- a/src/CubicalHott/Lemma2-4-3.agda +++ b/src/CubicalHott/Lemma2-4-3.agda @@ -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 diff --git a/src/CubicalHott/Lemma7-2-4.agda b/src/CubicalHott/Lemma7-2-4.agda new file mode 100644 index 0000000..60818e8 --- /dev/null +++ b/src/CubicalHott/Lemma7-2-4.agda @@ -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) \ No newline at end of file diff --git a/src/CubicalHott/Theorem2-7-2.agda b/src/CubicalHott/Theorem2-7-2.agda index ef4ac2a..e0db077 100644 --- a/src/CubicalHott/Theorem2-7-2.agda +++ b/src/CubicalHott/Theorem2-7-2.agda @@ -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 diff --git a/src/CubicalHott/Theorem7-1-11.agda b/src/CubicalHott/Theorem7-1-11.agda index de1ca70..0bd13db 100644 --- a/src/CubicalHott/Theorem7-1-11.agda +++ b/src/CubicalHott/Theorem7-1-11.agda @@ -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 = {! !} - \ No newline at end of file + \ No newline at end of file diff --git a/src/CubicalHott/Theorem7-1-4.agda b/src/CubicalHott/Theorem7-1-4.agda index f458e35..edde09c 100644 --- a/src/CubicalHott/Theorem7-1-4.agda +++ b/src/CubicalHott/Theorem7-1-4.agda @@ -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 diff --git a/src/CubicalHott/Theorem7-1-7.agda b/src/CubicalHott/Theorem7-1-7.agda index 2b54069..c5cca59 100644 --- a/src/CubicalHott/Theorem7-1-7.agda +++ b/src/CubicalHott/Theorem7-1-7.agda @@ -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 \ No newline at end of file diff --git a/src/CubicalHott/Theorem7-1-8.agda b/src/CubicalHott/Theorem7-1-8.agda index 166bf35..2018a85 100644 --- a/src/CubicalHott/Theorem7-1-8.agda +++ b/src/CubicalHott/Theorem7-1-8.agda @@ -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 diff --git a/src/CubicalHott/Theorem7-1-9.agda b/src/CubicalHott/Theorem7-1-9.agda index c344836..2d62726 100644 --- a/src/CubicalHott/Theorem7-1-9.agda +++ b/src/CubicalHott/Theorem7-1-9.agda @@ -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) diff --git a/src/CubicalHott/Theorem7-2-2.agda b/src/CubicalHott/Theorem7-2-2.agda index be5d13d..7fac66a 100644 --- a/src/CubicalHott/Theorem7-2-2.agda +++ b/src/CubicalHott/Theorem7-2-2.agda @@ -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 = - {! !} \ No newline at end of file +theorem R f1 f2 x y p q = {! !} \ No newline at end of file