From 2e416a404ffaf89089f3843921f58cc8d7a467d1 Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Mon, 22 Apr 2024 01:45:52 +0000 Subject: [PATCH] auto gitdoc commit --- src/HottBook/Chapter2Exercises.lagda.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/HottBook/Chapter2Exercises.lagda.md b/src/HottBook/Chapter2Exercises.lagda.md index 0aa85c6..03c63e2 100644 --- a/src/HottBook/Chapter2Exercises.lagda.md +++ b/src/HottBook/Chapter2Exercises.lagda.md @@ -9,8 +9,8 @@ open import HottBook.Util ## Exercise 2.4 -Define, by induction on n, a general notion of n-dimensional path in a type A, -simultaneously with the type of boundaries for such paths. +_Define, by induction on n, a general notion of n-dimensional path in a type +$A$, simultaneously with the type of boundaries for such paths._ (tracked in [#6][6]) @@ -29,7 +29,7 @@ Prove that the functions [2.3.6] and [2.3.7] are inverse equivalences. ### Exercise 2.13 -Show that (2 ≃ 2) ≃ 2. +_Show that $(2 \simeq 2) \simeq 2$._ ``` exercise2∙13 : (𝟚 ≃ 𝟚) ≃ 𝟚