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