Definition LRB_associator_comp_r' {a b c d e : B} (f0 : hom a b) (g0 : hom b c) (h0 : hom c d) (i0 : hom d e) : R (hom a e) ⟦ η (hom a e) (f0 · (g0 · (h0 · i0))), LRB_composition a b e (η (hom a b) f0, LRB_composition b c e (η (hom b c) g0, LRB_composition c d e (η (hom c d) h0, η (hom d e) i0)))⟧. Proof. use (_ · _). 3: { use (#(LRB_composition a b e)). 2: { use catbinprodmor. 3: apply identity. 2: { use (#(LRB_composition b c e)). 2: { use catbinprodmor. 3: apply identity. 2: exact (pr1 (nat_z_iso_inv (LRB_composition_comm c d e)) (h0,i0)). } } } } use (_ · _). 3: { use (#(LRB_composition a b e)). 2: { use catbinprodmor. 3: apply identity. 2: exact (pr1 (nat_z_iso_inv (LRB_composition_comm b c e)) (g0,h0 · i0 : hom _ _)). } } exact (pr1 (nat_z_iso_inv (LRB_composition_comm a b e)) (f0, g0 · (h0 · i0) : hom _ _)). 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.