Lemma are_inverses_from_Cokernel_to_Cokernel {y z : C} {g : y --> z} (CK CK': Cokernel g) : is_inverse_in_precat (from_Cokernel_to_Cokernel CK CK') (from_Cokernel_to_Cokernel CK' CK). Proof. split. - unfold from_Cokernel_to_Cokernel. apply pathsinv0. use CokernelEndo_is_identity. rewrite assoc. rewrite CokernelCommutes. rewrite CokernelCommutes. apply idpath. - unfold from_Cokernel_to_Cokernel. apply pathsinv0. use CokernelEndo_is_identity. rewrite assoc. rewrite CokernelCommutes. rewrite CokernelCommutes. apply idpath. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Epis. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Require Import UniMath.CategoryTheory.Limits.Zero. - exact (ZeroArrowFrom w). - intros y X. cbn in X. use ArrowsFromZero.