Lemma pair_functor_composite {C1 C2 C3 D1 D2 D3 : category} (F1 : functor C1 C2) (G1 : functor D1 D2) (F2 : functor C2 C3) (G2 : functor D2 D3) : nat_z_iso (functor_composite (pair_functor F1 G1) (pair_functor F2 G2)) (pair_functor (functor_composite F1 F2) (functor_composite G1 G2)). Proof. use make_nat_z_iso. { apply nat_trans_id. } intro. use tpair. - use catbinprodmor ; apply identity. - split ; apply id_right. 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.