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

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

@ -56,10 +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 (λ the what → (x , u) ≡ (the , transport P what u)) p refl
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
```
Verifying its property:
@ -99,12 +101,12 @@ transportconst {l₁} {l₂} {A} {x} {y} B p b =
### Lemma 2.3.8
```
lemma238 : {l : Level} {A B : Set l}
lemma2∙3∙8 : {l : Level} {A B : Set l}
→ (f : A → B)
→ {x y : A}
→ (p : x ≡ y)
→ apd f p ≡ transportconst B p (f x) ∙ ap f p
lemma238 {l} {A} {B} f {x} {y} p =
lemma2∙3∙8 {l} {A} {B} f {x} {y} p =
J (λ x y p → apd f p ≡ transportconst B p (f x) ∙ ap f p) (λ x → refl) x y p
```