Definition free_forgetful_are_adjoints : are_adjoints free_Alg forget_Alg. Proof. use make_are_adjoints. - apply (make_nat_trans _ _ (η T)). intros X Y f. apply η. - use make_nat_trans. + intro X. exact (Alg_map T (X : Algebra T),, Algebra_multlaw T X). + intros X Y f. apply Algebra_mor_eq; cbn. apply pathsinv0. apply f. - abstract (split; intro X; [apply Algebra_mor_eq; cbn; apply Monad_law2 | apply Algebra_idlaw]). Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Monads.Monads. Require Import UniMath.CategoryTheory.Monads.Derivative.