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