Definition actionbasedstrongmonads_cat_disp : disp_cat (category_Monad C). Proof. use tpair. - use tpair. + use make_disp_cat_ob_mor. * intro M. exact (∑ Ml : lineator_lax Mon_V Act Act (M: Monad C), ηandμlinear Ml). * intros M N [Ml islinM] [Nl islinN] α. exact (is_linear_nat_trans Ml Nl (nat_trans_from_monad_mor _ _ α)). + split. * intros M [Ml [islinMη islimMμ]]. cbn. apply is_linear_nat_trans_identity. * intros M N O α α' Mll Nll Oll islntα islntβ. exact (is_linear_nat_trans_comp (pr1 Mll) (pr1 Nll) (pr1 Oll) islntα islntβ). - repeat split; intros; try apply isaprop_is_linear_nat_trans. apply isasetaprop; apply isaprop_is_linear_nat_trans. Defined.
Require Import UniMath.Foundations.All. 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.Core.Isos. Require Import UniMath.CategoryTheory.Monads.Monads. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Functors. Require Import UniMath.CategoryTheory.Actegories.Actegories. Require Import UniMath.CategoryTheory.Actegories.MorphismsOfActegories. Require Import UniMath.CategoryTheory.Actegories.ConstructionOfActegories. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Import BifunctorNotations. Import MonoidalNotations. Import ActegoryNotations.