{X Y : Type} (f : X -> Y) {Ys : IsHSet Y} {wc : WeaklyConstant f} : merely X -> Y := (cconst_wconst_hset f).
Require Import HoTT.Basics HoTT.Types. Require Import Extensions Factorization. Require Import Truncations.Core Modalities.Modality.