proposition: Lemma right_unitor_naturality {C : prebicategory} {a b : C} (f g : a -1-> b) (alpha : f -2-> g) : whisker_right alpha (identity1 _) ;v; right_unitor g = right_unitor f ;v; alpha.
proof: Proof. intermediate_path ((functor_on_morphisms (functor_composite (bindelta_pair_functor (functor_identity _) (functor_composite (functor_to_unit _) (constant_functor unit_category _ (identity1 b)))) (compose_functor a b b)) alpha) ;v;(right_unitor _)). reflexivity. intermediate_path (right_unitor f ;v; functor_on_morphisms (functor_identity _) alpha). apply (nat_trans_ax (right_unitor_trans a b)). 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