IsPreIdempotent f. Proof. intros Z. apply path_baut. unfold f; simpl. refine (_ oE equiv_sum_assoc Z Cantor Cantor). apply (1 +E equiv_cantor_fold). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Idempotents. Require Import HoTT.Truncations.Core Universes.BAut Spaces.Cantor.