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