Definition reindexed_action_convertor : action_convertor Mon_V C reindexed_odot. Proof. exists reindexed_action_convertor_nat_trans. intro x. pose (k := ob1 (ob1 x)); pose (k' := ob2 (ob1 x)); pose (k'' := ob2 x). use is_z_isomorphism_comp. - exact (pr2 (act_χ actA) ((k, U k'), U k'')). - use is_z_iso_odot_z_iso. + use identity_is_z_iso. + exact (strong_monoidal_functor_μ_is_nat_z_iso U (k', k'')). 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.