(x : Cantor + Cantor + Cantor + Cantor) : (ff_flip x = x) <-> (is_inr x + is_inl_and is_inr x). Proof. split; intros p; destruct x as [[[c|c]|c]|c]; simpl in p. - do 2 apply path_sum_inl in p. elim (inl_ne_inr _ _ p^). - do 2 apply path_sum_inl in p. elim (inl_ne_inr _ _ p). - exact (inr tt). - exact (inl tt). - destruct p as [e|e]; elim e. - destruct p as [e|e]; elim e. - destruct p as [e|_]; [ elim e | reflexivity ]. - destruct p as [_|e]; [ reflexivity | elim e ]. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Idempotents. Require Import HoTT.Truncations.Core Universes.BAut Spaces.Cantor.