(Z Z' : BAut Cantor) (e : Z <~> Z') : I Z' oE (e +E 1 +E 1) = (e +E 1) oE I Z. Proof. revert e; equiv_intro (equiv_path Z Z') q. revert q; equiv_intro ((equiv_path_sigma_hprop Z Z')^-1) p. simpl. rewrite <- ap_ff, <- ap_f. unfold I. refine ((equiv_path_pp _ _)^ @ _ @ (equiv_path_pp _ _)). apply ap. refine ((pr1_path_pp (ap (f o f) p) (Ip Z'))^ @ _ @ pr1_path_pp _ _). apply ap. apply (concat_Ap Ip). Qed.
Require Import HoTT.Basics HoTT.Types. Require Import Idempotents. Require Import HoTT.Truncations.Core Universes.BAut Spaces.Cantor.