Definition Coalgebra_mor_commutes {X Y : Coalgebra} (f : Coalgebra_mor X Y) : f · Coalg_map Y = Coalg_map X · #T f := pr2 f.
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.