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:22:34 +00:00
parent cc2bff5cb1
commit 88fcab2a06
2 changed files with 12 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
.vscode/settings.json vendored
View file

@ -1,6 +1,6 @@
{
"editor.unicodeHighlight.ambiguousCharacters": false,
"gitdoc.enabled": true,
"gitdoc.autoCommitDelay": 120000,
"gitdoc.autoCommitDelay": 300000,
"gitdoc.commitMessageFormat": "'auto gitdoc commit'"
}

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

@ -174,14 +174,21 @@ _∼_ {l₁} {l₂} {A} {P} f g = (x : A) → f x ≡ g x
Homotopy forms an equivalence relation:
```
∼-refl : {A : Set} {P : A → Set} (f : (x : A) → P x) → f ∼ f
∼-refl : {A : Set} {P : A → Set}
→ (f : (x : A) → P x)
→ f ∼ f
∼-refl f x = refl
∼-sym : {A : Set} {P : A → Set} (f g : (x : A) → P x) → f ∼ g → g ∼ f
∼-sym : {A : Set} {P : A → Set}
→ (f g : (x : A) → P x)
→ f ∼ g → g ∼ f
∼-sym f g f∼g x = sym (f∼g x)
∼-trans : {A : Set} {P : A → Set} (f g h : (x : A) → P x)
→ f ∼ g → g ∼ h → f ∼ h
∼-trans : {A : Set} {P : A → Set}
→ (f g h : (x : A) → P x)
→ f ∼ g
→ g ∼ h
→ f ∼ h
∼-trans f g h f∼g g∼h x = f∼g x ∙ g∼h x
```