Definition functor_to_eilenberg_moore_cat_enrichment : functor_enrichment (functor_to_eilenberg_moore_cat M F τ τη τμ) E' eilenberg_moore_enrichment. Proof. simple refine (_ ,, _ ,, _ ,, _). - exact functor_to_em_enrichment_mor. - abstract (intros x ; use (dialgebra_enrichment_mor_eq_of_mor V HV EM (functor_id_enrichment _)) ; cbn ; rewrite !assoc' ; rewrite functor_to_em_enrichment_mor_incl ; refine (_ @ !(dialgebra_enrichment_id_incl _ _ _ _ _)) ; apply (functor_enrichment_id FE)). - abstract (intros x y z ; use (dialgebra_enrichment_mor_eq_of_mor V HV EM (functor_id_enrichment _)) ; cbn ; rewrite !assoc' ; rewrite functor_to_em_enrichment_mor_incl ; rewrite dialgebra_enrichment_comp_incl ; refine (functor_enrichment_comp FE x y z @ _) ; unfold dialgebra_enrichment_comp_mor ; rewrite !assoc ; apply maponpaths_2 ; refine (_ @ tensor_comp_mor _ _ _ _) ; rewrite !functor_to_em_enrichment_mor_incl ; apply idpath). - abstract (intros x y f ; use (dialgebra_enrichment_mor_eq_of_mor V HV EM (functor_id_enrichment _)) ; cbn ; rewrite !assoc' ; rewrite functor_to_em_enrichment_mor_incl ; refine (dialgebra_enrichment_from_arr_incl _ _ _ _ _ _ @ _) ; apply (functor_enrichment_from_arr FE)). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Subcategory.Core. Require Import UniMath.CategoryTheory.Subcategory.Full. Require Import UniMath.CategoryTheory.Categories.Dialgebras. Require Import UniMath.CategoryTheory.Categories.EilenbergMoore. Require Import UniMath.CategoryTheory.EnrichedCats.Enrichment. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentFunctor. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentTransformation. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentMonad. Require Import UniMath.CategoryTheory.EnrichedCats.Examples.DialgebraEnriched. Require Import UniMath.CategoryTheory.EnrichedCats.Examples.FullSubEnriched. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monads.Monads. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Terminal.