fact: Definition cconst_wconst_collapsible {X Y : Type} (f : X -> Y) `{Collapsible X} `{WeaklyConstant _ _ f} : ConditionallyConstant f.
imports: HoTT.Basics HoTT.Types Extensions Factorization Truncations.Core Modalities.Modality