Definition pair_nat_trans {C1 C2 D1 D2 : category} {F1 G1 : functor C1 D1} {F2 G2 : functor C2 D2} (α : nat_trans F1 G1) (β : nat_trans F2 G2) : nat_trans (pair_functor F1 F2) (pair_functor G1 G2). Proof. use make_nat_trans. - intro x. use catbinprodmor. + exact (α (pr1 x)). + exact (β (pr2 x)). - abstract (intro ; intros ; use total2_paths_f ; [ apply (pr2 α) | rewrite transportf_const ; apply (pr2 β) ] ). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored.