(X : Type@{i}) : Idempotent@{i i j} X := (idmap ; isidem_idmap X).
Require Import HoTT.Basics HoTT.Types. Require Import HFiber Constant. Require Import Truncations.Core Modalities.Modality. Require Import Homotopy.IdentitySystems.