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

proved theorem 7.1.10, closes #34

Browse source
This commit is contained in:
Michael Zhang 2024-10-20 03:06:06 -05:00
parent 607d75a99a
commit 136d9f67c3
1 changed files with 6 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -6,9 +6,11 @@ open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Data.Nat
z = isContr
open import CubicalHott.Lemma3-11-4 renaming (lemma to lemma3-11-4)
theorem : {X : Type} → (n : ℕ) → isProp (isOfHLevel n X)
theorem zero = {! !}
theorem (suc zero) x y = {! !}
theorem (suc (suc n)) x y = {! !}
theorem zero = lemma3-11-4
theorem (suc zero) isProp1 isProp2 i x y j = isProp→isSet isProp1 x y (isProp1 x y) (isProp2 x y) i j
theorem {X = X} (suc (suc n)) isHLevel1 isHLevel2 =
let IH = λ (x y : X) → theorem {X = x ≡ y} (suc n) in
funExt (λ x → funExt (λ y → IH x y (isHLevel1 x y) (isHLevel2 x y)))