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

solved lemma 3.11.4, closes #41

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

24
src/CubicalHott/Lemma3-11-4.agda
View file

@ -7,13 +7,29 @@ open import CubicalHott.Example3-6-2 renaming (example to example3-6-2)
lemma : {A : Type} → isProp (isContr A)
lemma {A} A-contr-x @ (x , px) (y , py) i =
let A-is-set = isProp→isSet (isContr→isProp A-contr-x) in
px y i , goal i where
A-is-set = isProp→isSet (isContr→isProp A-contr-x)
helper2 : px y i ≡ y
helper2 = sym (py (px y i))
helper1 : isProp ((z : A) → px y i ≡ z)
helper1 = example3-6-2 (λ x → isContr→isProp {! !})
helper1 = example3-6-2 (λ z → isContr→isProp (helper2 ∙ py z , λ q → A-is-set (px y i) z (helper2 ∙ py z) q))
wtf : (z : A) → sym (px z) ∙∙ px y ∙∙ py z ≡ refl {x = z}
wtf z = A-is-set z z (sym (px z) ∙∙ px y ∙∙ py z) refl
helper3 : (z : A) → PathP (λ i → px z i ≡ py z i) (px y) (sym (px z) ∙∙ px y ∙∙ py z)
helper3 z = doubleCompPath-filler (sym (px z)) (px y) (py z)
helper5 : (z : A) → PathP (λ i → px z i ≡ py z i) (px y) (refl {x = z})
helper5 z = helper3 z ▷ wtf z
goal2 : (z : A) → PathP (λ i → px y i ≡ z) (px z) (py z)
goal2 z i j = helper5 z j i
goal : PathP (λ i → (z : A) → px y i ≡ z) px py
goal i z = {! helper1 !}
goal i z j = funExt (λ z → goal2 z i) j z
-- λ y' j → isProp→isSet (isContr→isProp A-contr-x) (px y i) y' {! !} {! !} j i
-- λ y' j → isProp→isSet (isContr→isProp A-contr-x) (px y i) y' {! !} {! !} j i