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