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

auto gitdoc commit

Browse source
This commit is contained in:
Michael Zhang 2024-04-22 01:37:40 +00:00
parent c642f47288
commit c10e2405f8
1 changed files with 10 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -87,17 +87,17 @@ apd {l₁} {l₂} {A} {P} {x} {y} f p =
TODO
```
-- transportconst : {A : Set} {x y : A} (B : Set) → (p : x ≡ y) → (b : B)
-- → transport (λ _ → B) p b ≡ b
-- transportconst {A} {x} B p b =
-- let
-- D : (x y : A) → (p : x ≡ y) → Set
-- D x y p = transport (λ _ → B) p b ≡ b
transportconst : {A : Set} {x y : A} (B : Set) → (p : x ≡ y) → (b : B)
→ transport (λ _ → B) p b ≡ b
transportconst {A} {x} B p b =
let
D : (x y : A) → (p : x ≡ y) → Set
D x y p = transport (λ _ → B) p b ≡ b
-- d : (x : A) → D x x refl
-- d x = refl
-- in
-- J (λ x p → transport (λ _ → B) p b ≡ b) p (d x)
d : (x : A) → D x x refl
d x = refl
in
J (λ x p → transport (λ _ → B) p b ≡ b) p (d x)
```
### Lemma 2.3.8