From acbb85481fc854de46d703748d5bbed2d5f593a8 Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Wed, 24 Jul 2024 21:16:47 -0500 Subject: [PATCH] exercise 2.4 --- src/HottBook/Chapter2Exercises.lagda.md | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/src/HottBook/Chapter2Exercises.lagda.md b/src/HottBook/Chapter2Exercises.lagda.md index e643115..c3874b1 100644 --- a/src/HottBook/Chapter2Exercises.lagda.md +++ b/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