(X : Type) : QuasiIdempotent X. Proof. exists (preidem_idmap X); exact _. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Constant. Require Import Truncations.Core Modalities.Modality. Require Import Homotopy.IdentitySystems.