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:07:10 +00:00
parent 61649a0c57
commit 0cb341072c
1 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -56,12 +56,12 @@ transport {l₁} {l₂} {A} {x} {y} P p = J (λ x y p → P x → P y) (λ x →
TODO
```
lift : {A : Set} (P : A → Set) {x y : A}
→ (u : P x)
→ (p : x ≡ y)
→ (x , u) ≡ (y , transport P p u)
lift {A} P {x} {y} u p =
J (λ a b p → (a , {! !}) ≡ (b , {! !})) (λ x → {! !}) x y p
-- lift : {A : Set} (P : A → Set) {x y : A}
-- → (u : P x)
-- → (p : x ≡ y)
-- → (x , u) ≡ (y , transport P p u)
-- lift {A} P {x} {y} u p =
-- J (λ a b p → (x , {! !}) ≡ (y , {! !})) (λ x → {! !}) x y p
```
Verifying its property: