`{Funext} {X Y : Type} (f : X -> Y) (P : Type) {Pc : X -> Contr P} (g : X -> P) (h : P -> Y) (p : h o g == f) : ConditionallyConstant f. Proof. assert (merely X -> IsHProp P). { apply Trunc_rec. intros x; pose (Pc x); apply istrunc_succ. } pose (g' := Trunc_ind (fun _ => P) g : merely X -> P). exists (h o g'); intros x. apply p. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions Factorization. Require Import Truncations.Core Modalities.Modality.