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₂.
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.