{X Y : Type} `{Collapsible X} (f : X -> Y) {wc : WeaklyConstant f} : ConditionallyConstant f. Proof. exists (f o splitsupp_collapsible); intros x. unfold splitsupp_collapsible; simpl. apply wconst. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions Factorization. Require Import Truncations.Core Modalities.Modality.