Lemma Strong_Functor_category_Hstandard (F : [A, A']) (sη sη' : actionbased_strength Mon_V actn actn' F) : (∏ (a : A) (v : Mon_V), Strong_Functor_Category_mor_diagram (F,,sη) (F,,sη') (id F) a v) → (∏ (a : A) (v : Mon_V), Strong_Functor_Category_mor_diagram (F,,sη') (F,,sη) (id F) a v) → sη = sη'. Proof. intros leq geq. apply actionbased_strength_eq. apply nat_trans_eq_alt. intro av. assert (leqinst := leq (pr1 av) (pr2 av)). clear leq geq. etrans. { apply pathsinv0. apply id_right. } etrans. { exact leqinst. } clear leqinst. etrans. 2: { apply id_left. } apply cancel_postcomposition. show_id_type. change (# odot' (id (pr1 F (pr1 av), pr2 av)) = id actionbased_strength_dom Mon_V actn' F av). rewrite functor_id. apply idpath. Qed.
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.NaturalTransformations. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.SIP. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored. Require Import UniMath.Bicategories.MonoidalCategories.Actions. Require Import UniMath.Bicategories.MonoidalCategories.ActionBasedStrength.