Definition monoidal_cat_co_eilenberg_moore : monoidal _ := monoidal_fullsubcat mon_cat_co_eilenberg_moore_base mon_cat_co_eilenberg_moore_extra_condition unit_case tensor_case.
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.Categories.Dialgebras. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Functors. Require Import UniMath.CategoryTheory.Monoidal.Structure.Symmetric. Require Import UniMath.CategoryTheory.Monoidal.Examples.Fullsub. Require Import UniMath.CategoryTheory.Monoidal.FunctorCategories. Require Import UniMath.CategoryTheory.Monads.Comonads. Require Import UniMath.CategoryTheory.Monoidal.Examples.MonoidalDialgebras. Require Import UniMath.CategoryTheory.Monoidal.Examples.SymmetricMonoidalDialgebras. Require Import UniMath.CategoryTheory.Categories.CoEilenbergMoore. Import BifunctorNotations. Import MonoidalNotations.