fact: Definition morphism_prod {C : cartesian_category} {A1 B1 A2 B2 : C} (f:C⦅A1;B1⦆) (g:C⦅A2;B2⦆) : C⦅A1⨰A2;B1⨰B2⦆ := ⟪f∙projl|g∙projr⟫.
imports: Coq(ssreflect ssrfun) Coq.Classes(RelationClasses Morphisms) Relational(Category)