Definition LRB_associator_nat_z_iso_pre (x y z w : B) : nat_z_iso (pair_functor (η_{x,y}) (pair_functor (η_{y,z}) (η (hom z w))) ∙ (((precategory_binproduct_assoc (R (hom x y)) (R (hom y z)) (R (hom z w))) ∙ pair_functor (LRB_composition x y z) (functor_identity (R (hom z w)))) ∙ LRB_composition x z w) ) (pair_functor (η_{x,y}) (pair_functor (η_{y,z}) (η (hom z w))) ∙ (pair_functor (functor_identity (R (hom x y))) (LRB_composition y z w) ∙ LRB_composition x y w)). Proof. use (nat_z_iso_comp (nat_z_iso_functor_comp_assoc _ _ _)). transparent assert (p : (nat_z_iso (pair_functor (η_{x,y}) (pair_functor (η_{y,z}) (η (hom z w))) ∙ precategory_binproduct_assoc (R (hom x y)) (R (hom y z)) (R (hom z w))) (precategory_binproduct_assoc (hom x y) (hom y z) (hom z w) ∙ (pair_functor (pair_functor (η_{x,y}) (η_{y,z})) (η (hom z w)))))). { use make_nat_z_iso. - use make_nat_trans. + intro ; apply identity. + intro ; intros. cbn. do 3 rewrite id_left. now do 3 rewrite id_right. - intro ; apply (identity_is_z_iso (C := _ ⊠ _)). } transparent assert (q : (nat_z_iso (pair_functor (pair_functor (η_{x,y}) (η_{y,z})) (η (hom z w)) ∙ pair_functor (LRB_composition x y z) (functor_identity (R (hom z w)))) (pair_functor hcomp_functor (functor_identity (hom z w)) ∙ (pair_functor (η _) (η _))) ) ). { use (nat_z_iso_comp (nat_z_iso_inv (nat_z_iso_pair _ _ _ _))). use (nat_z_iso_comp _ (nat_z_iso_pair _ _ _ _)). use nat_z_iso_between_pair. - apply LRB_composition_comm. - apply functor_commutes_with_id. } transparent assert ( q' : (nat_z_iso ((pair_functor (functor_identity (hom x y)) hcomp_functor) ∙ pair_functor (η (hom _ _)) (η (hom _ _))) (pair_functor (η_{x,y}) (pair_functor (η_{y,z}) (η (hom z w))) ∙ pair_functor (functor_identity (R (hom x y))) (LRB_composition y z w)))). { use (nat_z_iso_comp (nat_z_iso_inv (nat_z_iso_pair _ _ _ _))). use (nat_z_iso_comp _ (nat_z_iso_pair _ _ _ _)). use nat_z_iso_between_pair. - apply functor_commutes_with_id. - apply nat_z_iso_inv, LRB_composition_comm. } use (nat_z_iso_comp (post_whisker_nat_z_iso _ _) _). 2: { use (nat_z_iso_comp (nat_z_iso_functor_comp_assoc _ _ _)). use (nat_z_iso_comp (post_whisker_nat_z_iso p _) _). use (nat_z_iso_comp (nat_z_iso_inv (nat_z_iso_functor_comp_assoc _ _ _))). apply (pre_whisker_nat_z_iso _ q). } use (nat_z_iso_comp (nat_z_iso_inv (nat_z_iso_functor_comp_assoc _ _ _))). use (nat_z_iso_comp (pre_whisker_nat_z_iso _ _) _). 2: { use (nat_z_iso_comp (nat_z_iso_inv (nat_z_iso_functor_comp_assoc _ _ _))). use (pre_whisker_nat_z_iso _ _). 2: apply LRB_composition_comm. } use (nat_z_iso_comp (pre_whisker_nat_z_iso _ _) _). 2: apply (nat_z_iso_functor_comp_assoc _ _ _). use (nat_z_iso_comp (nat_z_iso_functor_comp_assoc _ _ _)). use (nat_z_iso_comp (post_whisker_nat_z_iso _ _) _). 2: { use (nat_z_iso_comp (nat_z_iso_functor_comp_assoc _ _ _)). use tpair. - exact (rassociator_transf x y z w). - intro ; apply is_z_iso_rassociator. } use (nat_z_iso_comp _ (nat_z_iso_inv (nat_z_iso_functor_comp_assoc _ _ _))). use (nat_z_iso_comp _ (post_whisker_nat_z_iso q' _)). use (nat_z_iso_comp _ (nat_z_iso_functor_comp_assoc _ _ _)). use (nat_z_iso_comp _ (pre_whisker_nat_z_iso _ _)). 3: apply nat_z_iso_inv, LRB_composition_comm. apply nat_z_iso_inv, nat_z_iso_functor_comp_assoc. 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.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.Equivalences.CompositesAndInverses. Require Import UniMath.CategoryTheory.PrecompEquivalence. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.RezkCompletions.RezkCompletions. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Core.YonedaLemma. Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat. Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor. Require Import UniMath.Bicategories.PseudoFunctors.Properties. Require Import UniMath.Bicategories.PseudoFunctors.Examples.Composition.