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