(Z : BAut Cantor) : I Z +E 1 = I (f Z). Proof. unfold I; simpl. refine ((ap_f (Ip Z))^ @ _). do 2 apply ap. apply Jp. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Idempotents. Require Import HoTT.Truncations.Core Universes.BAut Spaces.Cantor.