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. 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.
Require Import UniMath.Foundations.PartD. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Categories.StandardCategories. Require Import UniMath.CategoryTheory.HorizontalComposition. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.Bicategories.WkCatEnrichment.prebicategory. Require Import UniMath.Bicategories.WkCatEnrichment.Notations.