csci8980-f21/extra/bin-suggestion.lagda.md

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 }
  }