fact: Definition morphism_class_intersection {C : category} (S T : morphism_class C) : morphism_class C := λ X Y f, (S _ _ f) ∧ (T _ _ f).
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.opp_precat UniMath.ModelCategories.Retract