split_idem (s o r) <~> A. Proof. simple refine (Build_Equiv _ _ (r o split_idem_sect (s o r)) (Build_IsEquiv _ _ _ (split_idem_retr (s o r) o s) _ _ _)). - intros a; simpl. refine (H _ @ H _). - intros a; simpl. refine (_ @ split_idem_issect (s o r) a). apply ap. refine ((split_idem_splits (s o r) _)^ @ _). apply ap, split_idem_issect; exact _. - intros a; simpl; apply equiv_split_idem_retract_isadj. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Constant. Require Import Truncations.Core Modalities.Modality. Require Import Homotopy.IdentitySystems.