BAut Cantor -> BAut Cantor. Proof. intros Z. exists (Z + Cantor). pose (e := Z.2); simpl in e; clearbody e. strip_truncations. apply tr. apply path_universe_uncurried. refine (equiv_cantor_fold oE _). refine (equiv_path _ _ e +E 1). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Idempotents. Require Import HoTT.Truncations.Core Universes.BAut Spaces.Cantor.