fact: Definition nat_trans_to_eilenberg_moore_cat_enrichment {C' : category} (E' : enrichment C' V) {F₁ F₂ : C' ⟶ eilenberg_moore_cat M} {FE₁ : functor_enrichment F₁ E' eilenberg_moore_enrichment} {FE₂ : functor_enrichment F₂ E' eilenberg_moore_enrichment} (τ : F₁ ∙ eilenberg_moore_pr M ⟹ F₂ ∙ eilenberg_moore_pr M) (Eτ : nat_trans_enrichment τ (functor_comp_enrichment FE₁ eilenberg_moore_pr_enrichment) (functor_comp_enrichment FE₂ eilenberg_moore_pr_enrichment)) (p : ∏ (x : C'), mor_of_eilenberg_moore_ob (F₁ x) · τ x = # M (τ x) · mor_of_eilenberg_moore_ob (F₂ x)) : nat_trans_enrichment (nat_trans_to_eilenberg_moore_cat M F₁ F₂ τ p) FE₁ FE₂.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Subcategory.Core UniMath.CategoryTheory.Subcategory.Full UniMath.CategoryTheory.Categories.Dialgebras UniMath.CategoryTheory.Categories.EilenbergMoore UniMath.CategoryTheory.EnrichedCats.Enrichment UniMath.CategoryTheory.EnrichedCats.EnrichmentFunctor UniMath.CategoryTheory.EnrichedCats.EnrichmentTransformation UniMath.CategoryTheory.EnrichedCats.EnrichmentMonad UniMath.CategoryTheory.EnrichedCats.Examples.DialgebraEnriched UniMath.CategoryTheory.EnrichedCats.Examples.FullSubEnriched UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monads.Monads UniMath.CategoryTheory.Limits.Equalizers UniMath.CategoryTheory.Limits.Terminal