Definition reindexed_action_right_unitor: action_right_unitor Mon_V C reindexed_odot. Proof. exists reindexed_action_right_unitor_nat_trans. intro. cbn. use is_z_isomorphism_comp. 2: { exact (pr2 (act_ϱ actA) c). } - use is_z_iso_odot_z_iso. + exact (identity_is_z_iso _ ). + apply (is_z_iso_inv_from_z_iso (strong_monoidal_functor_ϵ U)). Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalFunctorsTensored. Require Import UniMath.Bicategories.MonoidalCategories.Actions.