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

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

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