diff --git a/.vscode/settings.json b/.vscode/settings.json index 119b640..1369c2f 100644 --- a/.vscode/settings.json +++ b/.vscode/settings.json @@ -1,6 +1,6 @@ { "editor.unicodeHighlight.ambiguousCharacters": false, "gitdoc.enabled": true, - "gitdoc.autoCommitDelay": 120000, + "gitdoc.autoCommitDelay": 300000, "gitdoc.commitMessageFormat": "'auto gitdoc commit'" } diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md index 6c79ab6..c1ad14a 100644 --- a/src/HottBook/Chapter2.lagda.md +++ b/src/HottBook/Chapter2.lagda.md @@ -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 ```