split_idem_split' `{fs : Funext} {X : Type} (f : QuasiIdempotent X) : Splitting f := split_idem_split f.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Constant. Require Import Truncations.Core Modalities.Modality. Require Import Homotopy.IdentitySystems.