{X Y} (y : Y) : ConditionallyConstant (@const X Y y). Proof. exists (const y); intros x; reflexivity. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions Factorization. Require Import Truncations.Core Modalities.Modality.