Definition nat_trans_to_eilenberg_moore_cat {C₁ C₂ : category} (m : Monad C₂) (F₁ F₂ : C₁ ⟶ eilenberg_moore_cat m) (α : F₁ ∙ eilenberg_moore_pr m ⟹ F₂ ∙ eilenberg_moore_pr m) (p : ∏ (x : C₁), mor_of_eilenberg_moore_ob (F₁ x) · α x = # m (α x) · mor_of_eilenberg_moore_ob (F₂ x)) : F₁ ⟹ F₂. Proof. use make_nat_trans. - intro x. use make_mor_eilenberg_moore. + exact (α x). + exact (p x). - abstract (intros x y f ; use eq_mor_eilenberg_moore ; cbn ; exact (nat_trans_ax α _ _ f)). 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.Core.Univalence. Require Import UniMath.CategoryTheory.Categories.Dialgebras. Require Import UniMath.CategoryTheory.Subcategory.Core. Require Import UniMath.CategoryTheory.Subcategory.Full. Require Import UniMath.CategoryTheory.Monads.Monads.