{X Y : Type} (f : X -> Y) (P : Type) `{IsHProp P} (g : X -> P) (h : P -> Y) (p : h o g == f) : ConditionallyConstant f. Proof. pose (g' := Trunc_rec 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.