Lemma Cokernel_up_to_iso_isCokernel {x y z : C} (f : x --> y) (g : y --> z) (CK : Cokernel Z f) (h : z_iso CK z) (H : g = (CokernelArrow CK) · h) (H'' : f · g = ZeroArrow Z x z) : isCokernel Z f g H''. Proof. use (make_isCokernel). intros w h0 H'. use unique_exists. - exact ((inv_from_z_iso h) · (CokernelOut Z CK w h0 H')). - cbn. rewrite H. rewrite assoc. rewrite <- (assoc _ h). rewrite (is_inverse_in_precat1 h). rewrite id_right. use CokernelCommutes. - intros y0. apply hs. - intros y0 X. cbn beta in X. use (pre_comp_with_z_iso_is_inj h). rewrite assoc. set (tmp := maponpaths (λ gg : _, gg · CokernelOut Z CK w h0 H') (is_inverse_in_precat1 h)). cbn in tmp. use (pathscomp0 _ (! tmp)). clear tmp. rewrite id_left. use CokernelOutsEq. rewrite CokernelCommutes. rewrite assoc. rewrite <- X. apply cancel_postcomposition. rewrite H. apply cancel_precomposition. 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.