Definition boolascoprod: unit ⨿ unit ≃ bool. Proof. set (f := λ xx : coprod unit unit, match xx with ii1 t => true | ii2 t => false end). split with f. set (g := λ t:bool, match t with true => ii1 tt | false => ii2 tt end). assert (egf : ∏ xx : _, g (f xx) = xx). intro xx. induction xx as [ u | u ]. induction u. apply idpath. induction u. apply idpath. assert (efg : ∏ t : _, f (g t) = t). induction t. apply idpath. apply idpath. apply (isweq_iso f g egf efg). Defined.