exercise 2.4

src/HottBook/Chapter2Exercises.lagda.md

@@ -67,11 +67,9 @@ $A$, simultaneously with the type of boundaries for such paths._
 [6]: https://git.mzhang.io/school/type-theory/issues/6
 
 ```
--- data n-dimensional-path {A : Set} : (n : ℕ) → Set where
---   z : (x y : A) → x ≡ y → n-dimensional-path zero
---   s : (n : ℕ) → (d : n-dimensional-path {A} n) → n-dimensional-path (suc n)
--- n-dimensional-path {A} zero = (x y : A) → x ≡ y
--- n-dimensional-path {A} (suc n) = {!   !}
+data n-path {l : Level} : {A : Set l} → (x y : A) → Set (lsuc l) where
+  zero : {A : Set l} → {x y : A} → x ≡ y → n-path x y
+  suc : {A : Set l} → {x y : A} → {p q : x ≡ y} → p ≡ q → n-path p q
 ```
 
 ## Exercise 2.5