fact: Record FactorizationSystem@{i j k} := { class1 : forall {X Y : Type@{i}}, (X -> Y) -> Type@{j} ; ishprop_class1 : forall {X Y : Type@{i}} (g:X->Y), IsHProp (class1 g) ; class1_isequiv : forall {X Y : Type@{i}} (g:X->Y) {geq:IsEquiv g}, class1 g ; class1_compose : forall {X Y Z : Type@{i}} (g:X->Y) (h:Y->Z), class1 g -> class1 h -> class1 (h o g) ; class2 : forall {X Y : Type@{i}}, (X -> Y) -> Type@{k} ; ishprop_class2 : forall {X Y : Type@{i}} (g:X->Y), IsHProp (class2 g) ; class2_isequiv : forall {X Y : Type@{i}} (g:X->Y) {geq:IsEquiv g}, class2 g ; class2_compose : forall {X Y Z : Type@{i}} (g:X->Y) (h:Y->Z), class2 g -> class2 h -> class2 (h o g) ; factor : forall {X Y : Type@{i}} (f:X->Y), Factorization@{i} (@class1) (@class2) f ; path_factor : forall {X Y : Type@{i}} (f:X->Y) (fact : Factorization@{i} (@class1) (@class2) f) (fact' : Factorization@{i} (@class1) (@class2) f), PathFactorization@{i} fact fact' }.
imports: HoTT.Basics HoTT.Types Extensions PathAny