Lemma unassoc_commutes : nat_z_iso (HHH ∙ (precategory_binproduct_unassoc D D D)) ((precategory_binproduct_unassoc C C C) ∙ (pair_functor H HH)). 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.
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.Core.Univalence. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.catiso. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.PrecompEquivalence. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalFunctorCategory. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.TotalCategoryFacts. Require Import UniMath.CategoryTheory.Monoidal.RezkCompletion.LiftedTensor. Require Import UniMath.CategoryTheory.Monoidal.RezkCompletion.LiftedTensorUnit.