proposition: Lemma coalgebra_homo_commutes {X Y : coalgebra} (f : coalgebra_homo X Y) : (coalgebra_mor X) · #F f = f · (coalgebra_mor Y).
proof: Proof. exact (pr2 f). Defined.
imports: UniMath.Foundations.Propositions UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Limits.Terminal