fact: Definition preidem_baut_cantor_idem `{Univalence} : IsPreIdempotent baut_cantor_idem := BAut_Cantor_Idempotent.preidem_f.
imports: HoTT.Basics HoTT.Types Idempotents HoTT.Truncations.Core Spaces.BAut Spaces.Cantor