From dc32aadeb3774fbc004b764c89f92fae7d330a4a Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Mon, 22 Apr 2024 01:49:22 +0000
Subject: [PATCH] auto gitdoc commit

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

diff --git a/src/HottBook/Chapter2Exercises.lagda.md b/src/HottBook/Chapter2Exercises.lagda.md
index 03c63e2..379b4ff 100644
--- a/src/HottBook/Chapter2Exercises.lagda.md
+++ b/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 = {!   !}