tracking link

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 = {!   !}