proposition: Lemma associator_naturality {C : prebicategory} { a b c d : C } {f f' : a -1-> b} (alpha : f -2-> f') {g g' : b -1-> c} (beta : g -2-> g') {h h' : c -1-> d} (gamma : h -2-> h') : (alpha ;h; (beta ;h; gamma)) ;v; associator f' g' h' = associator f g h ;v; ((alpha ;h; beta) ;h; gamma).
proof: Proof. intermediate_path ((functor_on_morphisms (functor_composite (pair_functor (functor_identity _) (compose_functor b c d)) (compose_functor a b d)) (catbinprodmor alpha (catbinprodmor beta gamma))) ;v; associator f' g' h' ). reflexivity. intermediate_path (associator f g h ;v; (functor_on_morphisms (functor_composite (precategory_binproduct_assoc _ _ _) (functor_composite (pair_functor (compose_functor a b c) (functor_identity _)) (compose_functor a c d))) (catbinprodmor alpha (catbinprodmor beta gamma)))). apply (nat_trans_ax (associator_trans a b c d) _ _ (catbinprodmor alpha (catbinprodmor beta gamma))). reflexivity. Defined.
imports: UniMath.Foundations.PartD UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.Categories.StandardCategories UniMath.CategoryTheory.HorizontalComposition UniMath.CategoryTheory.Equivalences.Core UniMath.Bicategories.WkCatEnrichment.prebicategory UniMath.Bicategories.WkCatEnrichment.Notations