{X Y : Type} (f : X -> Y) {Ys : merely X -> IsHSet Y} {wc: WeaklyConstant f} : ConditionallyConstant f. Proof. srapply (cconst_factors_hprop f (image (-1) f)). - apply factor1. - apply factor2. - apply fact_factors. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions Factorization. Require Import Truncations.Core Modalities.Modality.