Cantor + Cantor -> Cantor. Proof. intros [c|c]; intros n. - destruct n as [|n]. + exact true. + exact (c n). - destruct n as [|n]. + exact false. + exact (c n). Defined.
Require Import HoTT.Basics HoTT.Types.