Definition actionbased_strength_from_relative_strength: actionbased_strength Mon_W' UAct UAct F. Proof. exists ϛ'. split. - red. cbn. intro v. change (str (monoidal_cat_unit Mon_W, v) · # F (# timesV (strong_monoidal_functor_ϵ_inv U #, id v) · lambda v) = # timesV (strong_monoidal_functor_ϵ_inv U #, id F v) · lambda (F v)). rewrite <- pentagon. rewrite assoc'. rewrite functor_comp. apply idpath. - cbn. apply actionbased_strength_pentagon_eq_fromvariant1. apply actionbased_strength_pentagon_eq_variant2variant1. red. intros v w' w. unfold ϛ', Mon_W', Mon_V', U'. cbn. unfold is_z_isomorphism_mor, pre_whisker_on_nat_z_iso. cbn. assert (Hyp := rectangle w w' v). fold timesV. fold timesW. fold alpha. change (str (timesW (w, w'), v) · # F (# timesV (strong_monoidal_functor_μ_inv U (w, w') #, id v) · alpha ((U w, U w'), v)) = # timesV (strong_monoidal_functor_μ_inv U (w, w') #, id F v) · alpha ((U w, U w'), F v) · # timesV (# U (id w) #, str (w', v)) · str (w, timesV (U w', v))). rewrite functor_id. rewrite functor_comp. rewrite assoc. exact Hyp. Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.HorizontalComposition. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Functors. Require Import UniMath.Bicategories.MonoidalCategories.EndofunctorsMonoidal. Require Import UniMath.Bicategories.MonoidalCategories.Actions. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalFunctorsTensored. Require Import UniMath.Bicategories.MonoidalCategories.EndofunctorsWhiskeredMonoidal. Require Import UniMath.Bicategories.Core.Bicat. Require Import UniMath.Bicategories.Core.Examples.BicatOfCats. Import MonoidalNotations. Import BifunctorNotations. Import MonoidalNotations.