Lemma LRB_lassociator_lassociator {a b c d e : B} (f : R (hom a b)) (g : R (hom b c)) (h : R (hom c d)) (i : R (hom d e)) : LRB_lwhisker f (inv_from_z_iso (LRB_associator g h i)) · (inv_from_z_iso (LRB_associator f (LRB_composition _ _ _ (g, h)) i)) · (LRB_rwhisker (inv_from_z_iso (LRB_associator f g h)) i) = inv_from_z_iso (LRB_associator f g (LRB_composition _ _ _ (h,i))) · inv_from_z_iso (LRB_associator (LRB_composition _ _ _ (f,g)) h i). Proof. use z_iso_inv_on_left. transparent assert (f_lw_a : (is_z_isomorphism (LRB_lwhisker f (inv_from_z_iso (LRB_associator g h i))))). { use functor_on_is_z_isomorphism. use is_z_iso_binprod_z_iso. - apply identity_is_z_iso. - apply is_z_iso_inv_from_z_iso. } transparent assert (r_a_i : (is_z_isomorphism (LRB_rwhisker (inv_from_z_iso (LRB_associator f g h)) i))). { use functor_on_is_z_isomorphism. use is_z_iso_binprod_z_iso. - apply is_z_iso_inv_from_z_iso. - apply identity_is_z_iso. } rewrite ! assoc'. use (z_iso_inv_to_left _ _ _ (_ ,, f_lw_a)). apply pathsinv0, z_iso_inv_on_left. rewrite ! assoc'. apply pathsinv0. use z_iso_inv_on_right. apply pathsinv0, (z_iso_inv_to_left _ _ _ (_ ,, r_a_i)). assert (p : inv_from_z_iso (LRB_rwhisker (inv_from_z_iso (LRB_associator f g h)) i,, r_a_i) = LRB_rwhisker (LRB_associator f g h) i). { apply idpath. } rewrite p. clear p. assert (p : inv_from_z_iso (LRB_lwhisker f (inv_from_z_iso (LRB_associator g h i)),, f_lw_a) = LRB_lwhisker f (LRB_associator g h i)). { apply idpath. } rewrite p. clear p. use (factor_through_squash _ _ (eso (hom _ _) f)). { apply homset_property. } intros [f0 pf]. induction (isotoid _ (pr2 (R (hom _ _))) pf). use (factor_through_squash _ _ (eso (hom _ _) g)). { apply homset_property. } intros [g0 pg]. induction (isotoid _ (pr2 (R (hom _ _))) pg). use (factor_through_squash _ _ (eso (hom _ _) h)). { apply homset_property. } intros [h0 ph]. induction (isotoid _ (pr2 (R (hom _ _))) ph). use (factor_through_squash _ _ (eso (hom _ _) i)). { apply homset_property. } intros [i0 pi]. induction (isotoid _ (pr2 (R (hom _ _))) pi). clear pf pg ph pi. clear f_lw_a r_a_i. etrans. { apply maponpaths, maponpaths_2. exact (LRB_associator_comp_m_on f0 g0 h0 i0). } etrans. 2: { apply maponpaths. exact (! LRB_associator_comp_r_on f0 g0 h0 i0). } etrans. 2: { apply maponpaths_2. exact (! LRB_associator_comp_l_on f0 g0 h0 i0). } etrans. 2: { rewrite assoc. apply maponpaths_2. rewrite assoc. apply maponpaths_2. rewrite assoc'. apply maponpaths, pathsinv0. unfold LRB_associator_comp_l', LRB_associator_comp_r. simpl. rewrite assoc. etrans. { apply maponpaths_2. rewrite assoc'. apply maponpaths. apply pathsinv0, (functor_comp (LRB_composition a c e)). } etrans. { apply maponpaths_2. do 2 apply maponpaths. simpl. cbn. etrans. { apply maponpaths. apply (pr2 (pr2 (LRB_composition_comm c d e) (h0, i0))). } apply maponpaths_2. apply (pr2 (pr2 (LRB_composition_comm a b c) (f0, g0))). } etrans. { apply maponpaths_2, maponpaths. apply (functor_id (LRB_composition a c e)). } rewrite id_right. apply (pr2 (LRB_composition_comm a c e) (f0 · g0 : hom _ _, h0 · i0 : hom _ _)). } rewrite id_right. etrans. 2: { apply maponpaths_2. rewrite assoc'. apply maponpaths. apply (functor_comp (η (hom a e))). } unfold LRB_associator_comp_l. etrans. { apply maponpaths_2. exact (LRB_lassociator_rwhisker_on f0 g0 h0 i0). } etrans. { rewrite assoc. apply maponpaths_2. rewrite assoc'. apply maponpaths. rewrite assoc. apply maponpaths_2. rewrite assoc. apply maponpaths_2. unfold LRB_lassociator_rwhisker', LRB_associator_comp_m. rewrite assoc. apply maponpaths_2. rewrite assoc'. apply maponpaths. etrans. { apply pathsinv0, (functor_comp (LRB_composition a d e)). } cbn. rewrite id_right. apply maponpaths, maponpaths_2. etrans. { apply pathsinv0, (functor_comp (LRB_composition a b d)). } rewrite <- binprod_comp. rewrite id_right. etrans. { do 2 apply maponpaths. apply (pr2 (pr2 (LRB_composition_comm b c d) (g0, h0))). } apply (functor_id (LRB_composition a b d)). } etrans. { apply maponpaths. exact (LRB_lassociator_lwhisker_on f0 g0 h0 i0). } etrans. 2: { apply maponpaths_2, maponpaths, maponpaths. exact (rassociator_rassociator f0 g0 h0 i0). } etrans. 2: { apply maponpaths_2, maponpaths. etrans. 2: apply pathsinv0, (functor_comp (η (hom _ _))). apply maponpaths_2. apply pathsinv0, (functor_comp (η (hom _ _))). } rewrite ! assoc. do 2 apply maponpaths_2. assert (q : # (η (hom a e)) (pr1 (rassociator_transf a b d e) (f0, (g0 · h0 : hom _ _, i0))) · LRB_associator_comp_m' f0 g0 h0 i0 · LRB_lassociator_lwhisker f0 g0 h0 i0 = # (η (hom a e)) (rassociator f0 (g0 · h0) i0)). { refine (_ @ id_right _). rewrite assoc'. apply maponpaths. unfold LRB_associator_comp_m'. unfold LRB_lassociator_lwhisker. etrans. { apply maponpaths_2. rewrite assoc'. apply maponpaths. etrans. { apply pathsinv0, functor_comp. } etrans. { apply maponpaths, pathsinv0, binprod_comp. } now rewrite id_right. } etrans. { rewrite assoc. apply maponpaths_2. rewrite assoc'. apply maponpaths. etrans. { apply pathsinv0, functor_comp. } etrans. { apply maponpaths, pathsinv0, binprod_comp. } rewrite id_right. do 2 apply maponpaths. rewrite assoc'. apply maponpaths. etrans. { apply pathsinv0, functor_comp. } etrans. { apply maponpaths, pathsinv0, binprod_comp. } rewrite id_right. etrans. { apply maponpaths, maponpaths_2. apply (pr2 (LRB_composition_comm b c d)). } apply (functor_id (LRB_composition b d e)). } rewrite id_right. etrans. { rewrite assoc. apply maponpaths_2. rewrite assoc'. apply maponpaths. etrans. { apply pathsinv0, functor_comp. } etrans. { apply maponpaths, pathsinv0, binprod_comp. } rewrite id_right. do 2 apply maponpaths. apply (pr2 (LRB_composition_comm b d e)). } rewrite (functor_id (LRB_composition a b e)). rewrite id_right. apply (pr2 (LRB_composition_comm a b e)). } rewrite <- q. rewrite ! assoc. do 3 apply maponpaths_2. unfold LRB_lassociator_rwhisker. rewrite ! assoc'. do 3 apply maponpaths. refine (_ @ id_right _). apply maponpaths. rewrite (functor_id (LRB_composition a d e)). rewrite id_left. etrans. { apply maponpaths. rewrite assoc. apply maponpaths_2. rewrite <- (functor_comp (LRB_composition a d e)). etrans. { apply maponpaths. rewrite <- binprod_comp. apply maponpaths_2. apply (pr2 (pr2 (LRB_composition_comm a b d) (f0 , g0 · h0 : hom _ _))). } rewrite id_right. apply (functor_id (LRB_composition a d e)). } rewrite id_left. apply (pr2 (pr2 (LRB_composition_comm a d e) (f0 · (g0 · h0) : hom _ _ , i0))). Qed.
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.