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. 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.
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.