(Z : BAut Cantor) : (Z + Cantor) + Cantor <~> Z + Cantor := equiv_path _ _ (Ip Z).
Require Import HoTT.Basics HoTT.Types. Require Import Idempotents. Require Import HoTT.Truncations.Core Universes.BAut Spaces.Cantor.