{Z Z' : BAut Cantor} (p : Z = Z') : equiv_path _ _ (ap (f o f) p)..1 = equiv_path Z Z' p..1 +E 1 +E 1. Proof. destruct p. apply path_equiv, path_arrow. intros [[z|a]|a]; reflexivity. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Idempotents. Require Import HoTT.Truncations.Core Universes.BAut Spaces.Cantor.