proposition: Lemma issig_Factorization : { I : Type & { g : A -> I & { h : I -> B & { p : h o g == f & { gin1 : class1 _ _ g & class2 _ _ h }}}}} <~> Factorization.
proof: Proof. issig. Defined.
imports: HoTT.Basics HoTT.Types Extensions PathAny