fact: Definition not_qidem_baut_cantor_idem `{Univalence} : ~ { I : IsPreIdempotent baut_cantor_idem & IsQuasiIdempotent baut_cantor_idem } := fun IJ => BAut_Cantor_Idempotent.impossible IJ.1 IJ.2.
imports: HoTT.Basics HoTT.Types Idempotents HoTT.Truncations.Core Spaces.BAut Spaces.Cantor