Definition product_of_commuting_squares {C1 C2 C3 C4 : category} {D1 D2 D3 D4 : category} {F1 : functor C1 C2} {F2 : functor C2 C4} {F1' : functor C1 C3} {F2' : functor C3 C4} {G1 : functor D1 D2} {G2 : functor D2 D4} {G1' : functor D1 D3} {G2' : functor D3 D4} (α : nat_z_iso (F1 ∙ F2) (F1' ∙ F2')) (β : nat_z_iso (G1 ∙ G2) (G1' ∙ G2')) : nat_z_iso (pair_functor F1 G1 ∙ pair_functor F2 G2) (pair_functor F1' G1' ∙ pair_functor F2' G2'). Proof. use make_nat_z_iso. - use make_nat_trans. + intro. use catbinprodmor. * apply α. * apply β. + abstract (intro ; intros ; use total2_paths_f ; [ apply (pr21 α) | rewrite transportf_const ; apply (pr21 β) ]). - intro. use is_z_iso_binprod_z_iso. + apply (pr2 α (pr1 _)). + apply (pr2 β (pr2 _)). 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.