RetractOf X := Build_RetractOf X split_idem split_idem_retr split_idem_sect split_idem_issect.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Constant. Require Import Truncations.Core Modalities.Modality. Require Import Homotopy.IdentitySystems.