proposition: Lemma unassoc_commutes {C D : category} (F : functor C D) : nat_z_iso ((pair_functor (pair_functor F F) F) ∙ (precategory_binproduct_unassoc D D D)) ((precategory_binproduct_unassoc C C C) ∙ (pair_functor F (pair_functor F F))).
proof: Proof. use make_nat_z_iso. - use make_nat_trans. + intro ; use catbinprodmor ; apply identity. + intro ; intros. use total2_paths_f. * exact (id_right _ @ ! id_left _). * abstract (rewrite transportf_const ; exact (id_right _ @ ! id_left _)). - intro. use tpair. * use catbinprodmor ; apply identity. * abstract (split ; (use total2_paths_f ; [ apply id_right | rewrite transportf_const ; apply id_right ])). Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.CategoryTheory.DisplayedCats.Univalence UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored