Martin Escardo. Notes originally written for the module Advanced Functional Programming of the University of Birmingham, UK.
The booleans are isomorphic to a Basic MLTT type:
open import isomorphisms
Bool-isomorphism : Bool ≅ 𝟙 ∔ 𝟙
Bool-isomorphism = record { bijection = f ; bijectivity = f-is-bijection }
where
f : Bool → 𝟙 ∔ 𝟙
f false = inl ⋆
f true = inr ⋆
g : 𝟙 ∔ 𝟙 → Bool
g (inl ⋆) = false
g (inr ⋆) = true
gf : g ∘ f ∼ id
gf true = refl true
gf false = refl false
fg : f ∘ g ∼ id
fg (inl ⋆) = refl (inl ⋆)
fg (inr ⋆) = refl (inr ⋆)
f-is-bijection : is-bijection f
f-is-bijection = record { inverse = g ; η = gf ; ε = fg }