Definition pair_functor {A B C D : category} (F : A ⟶ C) (G : B ⟶ D) : (A × B) ⟶ (C × D). Proof. apply (tpair _ (pair_functor_data F G)). abstract (split; [ intro x; simpl; rewrite !functor_id; apply idpath | intros x y z f g; simpl; rewrite !functor_comp; apply idpath]). 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.