Definition Coalgebra_mor_eq {X Y : Coalgebra T} {f g : Coalgebra_mor T X Y} : (f : X --> Y) = g ≃ f = g. Proof. apply invweq. apply subtypeInjectivity. intro h. apply homset_property. 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.