From 2be3dadbc8dc8cc1dc40a9176dae1c1dece575b1 Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Mon, 29 Apr 2024 14:42:34 -0400
Subject: [PATCH] tracking link

---
 src/HottBook/Chapter2Exercises.lagda.md | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/src/HottBook/Chapter2Exercises.lagda.md b/src/HottBook/Chapter2Exercises.lagda.md
index 079aa64..7bc4e42 100644
--- a/src/HottBook/Chapter2Exercises.lagda.md
+++ b/src/HottBook/Chapter2Exercises.lagda.md
@@ -14,7 +14,7 @@ $A$, simultaneously with the type of boundaries for such paths._
 
 (tracked in [#6][6])
 
-[6]: https://git.mzhang.io/school/cubical/issues/6
+[6]: https://git.mzhang.io/school/type-theory/issues/6
 
 ```
 
@@ -31,6 +31,10 @@ Prove that the functions [2.3.6] and [2.3.7] are inverse equivalences.
 
 _Show that $(2 \simeq 2) \simeq 2$._
 
+(tracked in [#8][8])
+
+[8]: https://git.mzhang.io/school/type-theory/issues/8
+
 lemma: equivalences are equal if their functions are equal
 
 ```
@@ -73,7 +77,7 @@ exercise2∙13 = f , equiv
     f∘g∼id false = refl
 
     g∘f∼id : g ∘ f ∼ id
-    g∘f∼id e' @ (f' , ie' @ (mkIsEquiv g' g-id h' h-id)) = {!   !}
+    g∘f∼id e' @ (f' , ie' @ (mkIsEquiv g' g-id h' h-id)) = attempt
       where
         f-codomain-is-2 : f' true ≢ f' false
         f-codomain-is-2 p = {!   !}