Definition Algebra_mor_comp (X Y Z : Algebra) (f : Algebra_mor X Y) (g : Algebra_mor Y Z) : Algebra_mor X Z. Proof. exists (f · g). abstract (unfold is_Algebra_mor; rewrite assoc; rewrite Algebra_mor_commutes; rewrite <- assoc; rewrite Algebra_mor_commutes; rewrite functor_comp, assoc; apply idpath). 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.