(x : Cantor + Cantor + Cantor + Cantor) : (ff_flip x = x) <-> (f_flip (I0 x) = I0 x). Proof. split; intros p. - refine ((I0nat_flip x)^ @ ap I0 p). - apply (equiv_inj I0). refine (I0nat_flip x @ p). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Idempotents. Require Import HoTT.Truncations.Core Universes.BAut Spaces.Cantor.