(a : split_idem) : split_idem_retr (split_idem_sect a) = a. Proof. refine (_ @ nudge_eq a); symmetry. simple refine (path_split_idem _ _). - exact (split_idem_issect_part1 a). - exact (split_idem_issect_part2 a). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Constant. Require Import Truncations.Core Modalities.Modality. Require Import Homotopy.IdentitySystems.