Definition pair_functor_data {A B C D : category} (F : A ⟶ C) (G : B ⟶ D) : functor_data (A × B) (C × D). Proof. use tpair. - intro x; apply (make_catbinprod (F (pr1 x)) (G (pr2 x))). - intros x y f; simpl; apply (catbinprodmor (# F (pr1 f)) (# G (pr2 f))). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.opp_precat.