(a : A) : split_idem_sect (s o r) (equiv_split_idem_retract^-1 a) = s a := ap s (H a).
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Constant. Require Import Truncations.Core Modalities.Modality. Require Import Homotopy.IdentitySystems.