`{Funext} (X Y : Type) : { f : X -> Y & ConditionallyConstant f } <~> (merely X -> Y). Proof. refine (_ oE (equiv_sigma_symm _)). refine (equiv_sigma_contr _). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions Factorization. Require Import Truncations.Core Modalities.Modality.