X -> split_idem. Proof. intros x. exists (fun n => f x). exact (fun n => I x). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Constant. Require Import Truncations.Core Modalities.Modality. Require Import Homotopy.IdentitySystems.