Definition LRB_associator_comp_l {a b c d e : B} (f : hom a b) (g : hom b c) (h : hom c d) (i : hom d e) : R (hom a e) ⟦ LRB_composition a d e (LRB_composition a c d (LRB_composition a b c (η (hom a b) f, η (hom b c) g), η (hom c d) h), η (hom d e) i), η (hom a e) ((f · g) · h · i) ⟧. Proof. use (_ · _). 2: { use (#(LRB_composition a d e)). 2: { use catbinprodmor. 4: apply identity. 2: { use (#(LRB_composition a c d)). 2: { use catbinprodmor. 4: apply identity. 2: exact (pr1 (LRB_composition_comm a b c) (f,g)). } } } } use (_ · _). 2: { use (#(LRB_composition a d e)). 2: { use catbinprodmor. 4: apply identity. 2: exact (pr1 (LRB_composition_comm a c d) (f·g : hom _ _,h)). } } exact (pr1 (LRB_composition_comm a d e) (f·g·h : hom _ _,i)). 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.