Cantor + Cantor + Cantor + Cantor <~> Cantor + Cantor + Cantor := I (f (point (BAut Cantor))).
Require Import HoTT.Basics HoTT.Types. Require Import Idempotents. Require Import HoTT.Truncations.Core Universes.BAut Spaces.Cantor.