From f2cb91fc30049be57bd314b172e140cdd0003413 Mon Sep 17 00:00:00 2001
From: wadler <wadler@inf.ed.ac.uk>
Date: Thu, 30 Apr 2020 08:36:48 -0300
Subject: [PATCH] added Levy suggestion to extra

---
 extra/bin-suggestion.lagda.md | 28 ++++++++++++++++++++++++++++
 extra/iso-exercise.lagda      |  3 ++-
 2 files changed, 30 insertions(+), 1 deletion(-)
 create mode 100644 extra/bin-suggestion.lagda.md

diff --git a/extra/bin-suggestion.lagda.md b/extra/bin-suggestion.lagda.md
new file mode 100644
index 00000000..4e5bad49
--- /dev/null
+++ b/extra/bin-suggestion.lagda.md
@@ -0,0 +1,28 @@
+Michel Levy has a suggestion for improving Bin in Quantifiers.
+
+In the Quantifiers chapter, I found the Bin-isomorphism exercise
+difficult. I suggest the following variation. A canonical element is an
+element (to n). Hence the alternative definition of Can.
+
+```
+data Can': Bin -> Set where
+  tocan : {b : Bin } -> ∃[ n ] (b ≡ to n) -> Can' b
+```
+
+With this definition the proof of the property, "if b is canonical, then
+`to (from b) = b`" becomes much simpler.
+```
+tofrom: (b: Bin) -> Can' b -> to (from b) ≡ b
+tofrom b (tocan ⟨ n , btn ⟩) =
+  Eq.trans (Eq.cong (to ∘ from) btn) (Eq.trans (Eq.cong to (fromto n)) (Eq.sym btn))
+
+ℕ≃Can : ℕ ≃ ∃[ b ] (Can' b)
+ℕ≃Can =
+  record  {
+  to = \ { n -> ⟨ to n , tocan ⟨ n , refl ⟩ ⟩}
+  ; from = \ { ⟨ _ , tocan ⟨ n , _ ⟩ ⟩ -> n }
+  ; from∘to = \ { n -> refl}
+  ; to∘from = \ { ⟨ _ , tocan ⟨ n , refl ⟩ ⟩ -> refl }
+  }
+```
+
diff --git a/extra/iso-exercise.lagda b/extra/iso-exercise.lagda
index 22de31b5..0ea8867d 100644
--- a/extra/iso-exercise.lagda
+++ b/extra/iso-exercise.lagda
@@ -1,4 +1,3 @@
-\begin{code}
 module iso-exercise where
 
 import Relation.Binary.PropositionalEquality as Eq
@@ -7,6 +6,8 @@ open Eq.≡-Reasoning
 open import plfa.Isomorphism using (_≃_)
 open import Data.List using (List; []; _∷_)
 open import Data.List.All using (All; []; _∷_)
+
+\begin{code}
 open import Data.List.Any using (Any; here; there)
 open import Data.List.Membership.Propositional using (_∈_)
 open import Function using (_∘_)