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

lemma 3.11.6

Browse source
This commit is contained in:
Michael Zhang 2024-07-11 00:31:26 -05:00
parent 3807a5759a
commit 1e270130e0
1 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/HottBook/Chapter3.lagda.md
View file

@ -417,7 +417,10 @@ lemma3∙11∙6 {A} {P} allContr =
let let
Pa-isProp : isProp ((x : A) → P x) Pa-isProp : isProp ((x : A) → P x)
Pa-isProp = example3∙6∙2 λ x → Σ.snd (lemma3∙11∙3.properties.ii (lemma3∙11∙3.i (allContr x))) Pa-isProp = example3∙6∙2 λ x → Σ.snd (lemma3∙11∙3.properties.ii (lemma3∙11∙3.i (allContr x)))
in {! !} , {! !}
center : (x : A) → P x
center x = Σ.fst (allContr x)
in center , λ x → Pa-isProp center x
``` ```
### Lemma 3.11.8 ### Lemma 3.11.8