(x : Cantor + Cantor + Cantor + Cantor) : (is_inr x + is_inl_and is_inr x) <-> is_inr (I0 x). Proof. refine (iff_compose _ (f_flip_fixed_iff_inr (I0 x))). refine (iff_compose _ (I0_fixed_iff_fixed x)). apply iff_inverse, ff_flip_fixed_iff_inr. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Idempotents. Require Import HoTT.Truncations.Core Universes.BAut Spaces.Cantor.