From c10e2405f835ab156bbc81a4a8a5b52d8db82de3 Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Mon, 22 Apr 2024 01:37:40 +0000
Subject: [PATCH] auto gitdoc commit

---
 src/HottBook/Chapter2.lagda.md | 20 ++++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md
index 8a1997c..c67aea4 100644
--- a/src/HottBook/Chapter2.lagda.md
+++ b/src/HottBook/Chapter2.lagda.md
@@ -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