Definition LRB_associator_pre_simpl_mor {x y z w : B} (f : B⟦x,y⟧) (g : B⟦y,z⟧) (h : B⟦z,w⟧) : R (hom x w) ⟦ (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)) (f : hom x y, (g : hom y z, h : hom 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)) (f : hom x y, (g : hom y z, h : hom z w)) ⟧. Proof. refine (#(LRB_composition x z w) (pr1 (LRB_composition_comm x y z) (f : hom _ _ , g : hom _ _) #, identity _) · _). refine (_ · #( LRB_composition x y w) (identity _ #, pr1 (nat_z_iso_inv (LRB_composition_comm y z w)) (g : hom _ _ , h : hom _ _))). cbn. refine (pr1 (LRB_composition_comm x z w) (f · g : hom _ _ , h : hom _ _) · _). refine (_ · pr1 (nat_z_iso_inv (LRB_composition_comm x y w)) (f : hom _ _ , g · h : hom _ _)). apply (#(η (hom x w))). exact (rassociator f g h). 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.