fact: Definition cconst_factors_hprop {X Y : Type} (f : X -> Y) (P : Type) `{IsHProp P} (g : X -> P) (h : P -> Y) (p : h o g == f) : ConditionallyConstant f.
imports: HoTT.Basics HoTT.Types Extensions Factorization Truncations.Core Modalities.Modality