Definition Coalgebra_mor_comp (X Y Z : Coalgebra) (f : Coalgebra_mor X Y) (g : Coalgebra_mor Y Z) : Coalgebra_mor X Z. Proof. exists (f · g). abstract (unfold is_Coalgebra_mor; rewrite assoc'; rewrite Coalgebra_mor_commutes; rewrite assoc; rewrite Coalgebra_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.Comonads.