(X : Type) (f : PreIdempotent X) (ss : forall x, Collapsible (f x = x)) : IsEmbedding (retract_sect (split_preidem_splitsupp X f ss).1). Proof. apply istruncmap_mapinO_tr; exact _. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Constant. Require Import Truncations.Core Modalities.Modality. Require Import Homotopy.IdentitySystems.