proposition: Theorem contr_factor `{Univalence} (factsys : FactorizationSystem) {X Y : Type} (f : X -> Y) : Contr (Factorization (@class1 factsys) (@class2 factsys) f).
proof: Proof. apply contr_inhabited_hprop. - apply hprop_allpath. intros fact fact'. apply path_factorization; try exact _. apply path_factor. - apply factor. Defined.
imports: HoTT.Basics HoTT.Types Extensions PathAny