{ I : Type & { g : A -> I & { h : I -> B & { p : h o g == f & { gin1 : class1 _ _ g & class2 _ _ h }}}}} <~> Factorization. Proof. issig. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Extensions Homotopy.IdentitySystems.