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

auto gitdoc commit

Browse source
This commit is contained in:
Michael Zhang 2024-04-22 02:21:09 +00:00
parent 0cb341072c
commit cc2bff5cb1
1 changed files with 7 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/HottBook/Chapter2.lagda.md
View file

@ -149,11 +149,13 @@ lemma2∙3∙8 {l} {A} {B} f {x} {y} p =
### Lemma 2.3.11
```
-- lemma2311 : {A : Set} {P Q : A → Set} (f : (x : A) → P x → Q x)
-- → {x y : A} (p : x ≡ y) → (u : P x)
-- → transport Q p (f x u) ≡ f y (transport P p u)
-- lemma2311 {A} {P} {Q} f {x} {y} p u =
-- J (λ the what → transport Q what (f x u) ≡ f the (transport P what u)) p refl
lemma2∙3∙11 : {A : Set} {P Q : A → Set}
→ (f : (x : A) → P x → Q x)
→ {x y : A} (p : x ≡ y) → (u : P x)
→ transport Q p (f x u) ≡ f y (transport P p u)
lemma2∙3∙11 {A} {P} {Q} f {x} {y} p u =
J (λ a b p → transport Q p (f a {! !}) ≡ f b (transport P p {! !})) (λ a → {! !}) x y p
-- J (λ the what → transport Q what (f x u) ≡ f the (transport P what u)) p refl
```
## 2.4 Homotopies and equivalences