auto gitdoc commit

src/HottBook/Chapter2Exercises.lagda.md

@@ -89,6 +89,8 @@ exercise2∙13 = aux1 , equiv1
         -- known that (f ∘ g) x ≡ x
         -- g (f x) ≡ x
         -- g (f true) ≡ true
+        -- maybe a proof by contradiction? suppose f true ≡ f false. why doesn't this work if f ∘ g ∼ id?
+        -- how to work backwards from the f ∘ g ∼ id? since we have a value `g-id` of that
         asdf true = {!   !}
         asdf false = {!   !}