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 01:39:32 +00:00
parent c10e2405f8
commit b99ce50aac
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

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