Library UniMath.CategoryTheory.limits.cokernels

Direct definition of cokernels

Contents

  • Definition of cokernel
  • Correspondence of cokernels and coequalizers
  • Cokernel up to iso
  • Cokernel of Epi · morphism
  • CokernelOut of equal morphisms

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.

Local Open Scope cat.

Definition of cokernels

Section def_cokernels.

  Context {C : category}.
  Let hs : has_homsets C := homset_property C.
  Hypothesis Z : Zero C.

Definition and construction of Cokernels
  Definition isCokernel {x y z : C} (f : x --> y) (g : y --> z) (H : f · g = (ZeroArrow Z x z)) : UU :=
    ∏ (w : C) (h : y --> w) (H : f · h = ZeroArrow Z x w), ∃! φ : z --> w, g · φ = h.

  Lemma isCokernel_paths {x y z : C} (f : x --> y) (g : y --> z) (H H' : f · g = (ZeroArrow Z x z))
        (isC : isCokernel f g H) : isCokernel f g H'.
  Proof.
    assert (e : H = H') by apply hs.
    induction e. exact isC.
  Qed.

  Local Lemma make_isCokernel_uniqueness {x y z : C} (f : x --> y) (g : y --> z)
        (H1 : f · g = ZeroArrow Z x z)
        (H2 : ∏ (w : C) (h : C ⟦ y, w ⟧),
              f · h = ZeroArrow Z x w → ∃! ψ : C ⟦ z, w ⟧, g · ψ = h)
        (w : C) (h : y --> w) (H' : f · h = ZeroArrow Z x w) :
    ∏ y0 : C ⟦ z, w ⟧, g · y0 = h → y0 = pr1 (iscontrpr1 (H2 w h H')).
  Proof.
    intros y0 H. apply (base_paths _ _ ((pr2 (H2 w h H')) (tpair _ y0 H))).
  Qed.

  Definition make_isCokernel {x y z : C} (f : x --> y) (g : y --> z) (H1 : f · g = ZeroArrow Z x z)
             (H2 : ∏ (w : C) (h : y --> w) (H' : f · h = ZeroArrow Z x w),
                   ∃! ψ : z --> w, g · ψ = h) : isCokernel f g H1.
  Proof.
    unfold isCokernel.
    intros w h H'.
    use unique_exists.
    - exact (pr1 (iscontrpr1 (H2 w h H'))).
    - exact (pr2 (iscontrpr1 (H2 w h H'))).
    - intros y0. apply hs.
    - intros y0 X. exact (base_paths _ _ ((pr2 (H2 w h H')) (tpair _ y0 X))).
  Defined.

  Definition Cokernel {x y : C} (f : x --> y) : UU :=
    ∑ D : (∑ z : ob C, y --> z),
          ∑ (e : f · (pr2 D) = ZeroArrow Z x (pr1 D)), isCokernel f (pr2 D) e.

  Definition make_Cokernel {x y z : C} (f : x --> y) (g : y --> z) (H : f · g = (ZeroArrow Z x z))
             (isCK : isCokernel f g H) : Cokernel f := ((z,,g),,(H,,isCK)).

  Definition Cokernels : UU := ∏ (x y : C) (f : x --> y), Cokernel f.

  Definition hasCokernels : UU := ∏ (x y : C) (f : x --> y), ishinh (Cokernel f).

  Definition CokernelOb {x y : C} {f : x --> y} (CK : Cokernel f) : ob C := pr1 (pr1 CK).
  Coercion CokernelOb : Cokernel >-> ob.

  Definition CokernelArrow {x y : C} {f : x --> y} (CK : Cokernel f) : C⟦y, CK⟧ := pr2 (pr1 CK).

  Definition CokernelCompZero {x y : C} {f : x --> y} (CK : Cokernel f) :
    f · (CokernelArrow CK) = (ZeroArrow Z x CK) := pr1 (pr2 CK).

  Definition CokernelisCokernel {y z : C} {g : y --> z} (CK : Cokernel g) := pr2 (pr2 CK).

  Definition CokernelOut {y z : C} {g : y --> z} (CK : Cokernel g) (w : C) (h : z --> w)
             (H : g · h = ZeroArrow Z y w) : C⟦CK, w⟧ :=
    pr1 (iscontrpr1 (CokernelisCokernel CK w h H)).

  Definition CokernelCommutes {y z : C} {g : y --> z} (CK : Cokernel g) (w : C) (h : z --> w)
        (H : g · h = ZeroArrow Z y w) : (CokernelArrow CK) · (CokernelOut CK w h H) = h
    := pr2 (iscontrpr1 (CokernelisCokernel CK w h H)).

  Local Lemma CokernelOutUnique {x y z : C} {f : x --> y} {g : y --> z} {H : f · g = ZeroArrow Z x z}
        (isCK : isCokernel f g H) {w : C} {h : y --> w} (H' : f · h = ZeroArrow Z x w) {φ : z --> w}
        (H'' : g · φ = h) :
    φ = (pr1 (pr1 (isCK w h H'))).
  Proof.
    exact (base_paths _ _ (pr2 (isCK w h H') (tpair _ φ H''))).
  Qed.

  Lemma CokernelOutsEq {x y : C} {f : x --> y} (CK : Cokernel f) {w : C} (φ1 φ2 : C⟦CK, w⟧)
        (H' : (CokernelArrow CK) · φ1 = (CokernelArrow CK) · φ2) : φ1 = φ2.
  Proof.
    assert (H1 : f · ((CokernelArrow CK) · φ1) = ZeroArrow Z _ _).
    {
      rewrite assoc. rewrite CokernelCompZero. apply ZeroArrow_comp_left.
    }
    rewrite (CokernelOutUnique (CokernelisCokernel CK) H1 (idpath _)).
    apply pathsinv0.
    set (tmp := pr2 (CokernelisCokernel CK w (CokernelArrow CK · φ1) H1) (tpair _ φ2 (! H'))).
    exact (base_paths _ _ tmp).
  Qed.

  Lemma CokernelOutComp {y z : C} {f : y --> z} (K : Cokernel f) {w w' : C} (h1 : z --> w)
        (h2 : w --> w') (H1 : f · (h1 · h2) = ZeroArrow Z _ _) (H2 : f · h1 = ZeroArrow Z _ _) :
    CokernelOut K w' (h1 · h2) H1 = CokernelOut K w h1 H2 · h2.
  Proof.
    use CokernelOutsEq. rewrite CokernelCommutes. rewrite assoc. rewrite CokernelCommutes.
    apply idpath.
  Qed.

Results on morphisms between Cokernels.
  Definition identity_is_CokernelOut {x y : C} {f : x --> y} (CK : Cokernel f) :
    ∑ φ : C⟦CK, CK⟧, (CokernelArrow CK) · φ = (CokernelArrow CK).
  Proof.
    ∃ (identity CK).
    apply id_right.
  Defined.

  Lemma CokernelEndo_is_identity {x y : C} {f : x --> y} {CK : Cokernel f} (φ : C⟦CK, CK⟧)
        (H : (CokernelArrow CK) · φ = CokernelArrow CK) : identity CK = φ.
  Proof.
    set (H1 := tpair ((fun φ' : C⟦CK, CK⟧ ⇒ _ · φ' = _)) φ H).
    assert (H2 : identity_is_CokernelOut CK = H1).
    - apply proofirrelevancecontr.
      apply (CokernelisCokernel CK).
      apply CokernelCompZero.
    - apply (base_paths _ _ H2).
  Qed.

  Definition from_Cokernel_to_Cokernel {x y : C} {f : x --> y} (CK CK': Cokernel f) : C⟦CK, CK'⟧.
  Proof.
    use (CokernelOut CK CK' (CokernelArrow CK')).
    use CokernelCompZero.
  Defined.

  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.

  Definition iso_from_Cokernel_to_Cokernel {y z : C} {g : y --> z} (CK CK' : Cokernel g) :
    z_iso CK CK' := make_z_iso (from_Cokernel_to_Cokernel CK CK') (from_Cokernel_to_Cokernel CK' CK)
                             (are_inverses_from_Cokernel_to_Cokernel CK CK').

Cokernel of the ZeroArrow is given by the identity.
  Lemma CokernelOfZeroArrow_isCokernel (x y : C) :
    isCokernel (ZeroArrow Z x y) (identity y) (id_right (ZeroArrow Z x y)).
  Proof.
    use make_isCokernel.
    intros w h H'.
    use unique_exists.
    - exact h.
    - exact (id_left _).
    - intros y0. apply hs.
    - intros y0 t. cbn in t. rewrite id_left in t. exact t.
  Qed.

  Definition CokernelofZeroArrow (x y : C) : Cokernel (ZeroArrow Z x y) :=
    make_Cokernel (ZeroArrow Z x y) (identity y) (id_right _) (CokernelOfZeroArrow_isCokernel x y).

Cokernel of identity is given by arrow to zero
  Local Lemma CokernelOfIdentity_isCokernel (x : C) :
    isCokernel (identity x) (ZeroArrowTo x)
               (ArrowsToZero C Z x (identity x · ZeroArrowTo x) (ZeroArrow Z x Z)).
  Proof.
    use make_isCokernel.
    intros w h H'.
    use unique_exists.
    - exact (ZeroArrowFrom w).
    - cbn. rewrite id_left in H'. rewrite H'. apply idpath.
    - intros y. apply hs.
    - intros y X. cbn in X. use ArrowsFromZero.
  Qed.

  Definition CokernelOfIdentity (x : C) : Cokernel (identity x).
  Proof.
    use make_Cokernel.
    - exact Z.
    - exact (ZeroArrowTo x).
    - use ArrowsToZero.
    - exact (CokernelOfIdentity_isCokernel x).
  Defined.

More generally, the CokernelArrow of the cokernel of the ZeroArrow is an isomorphism.
  Lemma CokernelofZeroArrow_is_iso {x y : C} (CK : Cokernel (ZeroArrow Z x y)) :
    is_inverse_in_precat (CokernelArrow CK)
                         (from_Cokernel_to_Cokernel CK (CokernelofZeroArrow x y)).
  Proof.
    use make_is_inverse_in_precat.
    - unfold from_Cokernel_to_Cokernel. rewrite CokernelCommutes. apply idpath.
    - unfold from_Cokernel_to_Cokernel. cbn.
      use CokernelOutsEq. rewrite assoc. rewrite CokernelCommutes.
      rewrite id_left. rewrite id_right. apply idpath.
  Qed.

  Definition CokernelofZeroArrow_iso (x y : C) (CK : Cokernel (ZeroArrow Z x y)) : z_iso y CK :=
    make_z_iso (CokernelArrow CK) (from_Cokernel_to_Cokernel CK (CokernelofZeroArrow x y))
             (CokernelofZeroArrow_is_iso CK).

It follows that CokernelArrow is an epi.
  Lemma CokernelArrowisEpi {y z : C} {g : y --> z} (CK : Cokernel g ) : isEpi (CokernelArrow CK).
  Proof.
    unfold isEpi.
    intros z0 g0 h X.
    use CokernelOutsEq.
    exact X.
  Qed.

  Lemma CokernelsOut_is_iso {x y : C} {f : x --> y} (CK1 CK2 : Cokernel f) :
    is_iso (CokernelOut CK1 CK2 (CokernelArrow CK2) (CokernelCompZero CK2)).
  Proof.
    use is_iso_qinv.
    - use CokernelOut.
      + use CokernelArrow.
      + use CokernelCompZero.
    - split.
      + use CokernelOutsEq. rewrite assoc. rewrite CokernelCommutes. rewrite CokernelCommutes.
        rewrite id_right. apply idpath.
      + use CokernelOutsEq. rewrite assoc. rewrite CokernelCommutes. rewrite CokernelCommutes.
        rewrite id_right. apply idpath.
  Qed.

End def_cokernels.
Arguments CokernelArrow [C] [Z] [x] [y] [f] _.
Arguments Cokernel [_] _ {_ _}.
Arguments isCokernel [_] _ {x y z}.
Arguments CokernelOut [_] _ {y z g}.
Arguments make_Cokernel [_] _ {x y z}.
Arguments CokernelCompZero [_] _ {x y f}.

Correspondence of cokernels and coequalizers

Section cokernels_coequalizers.

  Context (C : category).
  Let hs : has_homsets C := homset_property C.
  Hypothesis Z : Zero C.

Coequalizer from Cokernel

  Lemma CokernelCoequalizer_eq {x y : ob C} {f : x --> y} (CK : Cokernel Z f) :
    f · CokernelArrow CK = ZeroArrow Z x y · CokernelArrow CK.
  Proof.
    rewrite ZeroArrow_comp_left. use CokernelCompZero.
  Qed.

  Lemma CokernelCoequalizer_isCokernel {x y : ob C} {f : x --> y} (CK : Cokernel Z f) :
    isCoequalizer f (ZeroArrow Z x y) (CokernelArrow CK) (CokernelCoequalizer_eq CK).
  Proof.
    use make_isCoequalizer.
    intros w0 h H'.
    use unique_exists.
    - use CokernelOut.
      + exact h.
      + rewrite H'. apply ZeroArrow_comp_left.
    - use CokernelCommutes.
    - intros y0. apply hs.
    - intros y0 X. use CokernelOutsEq. rewrite CokernelCommutes. exact X.
  Qed.

  Definition CokernelCoequalizer {x y : ob C} {f : x --> y} (CK : Cokernel Z f) :
    Coequalizer f (ZeroArrow Z _ _).
  Proof.
    use make_Coequalizer.
    - exact CK.
    - exact (CokernelArrow CK).
    - exact (CokernelCoequalizer_eq CK).
    - exact (CokernelCoequalizer_isCokernel CK).
  Defined.

Cokernel from Coequalizer


  Lemma CoequalizerCokernel_eq {x y : ob C} {f : x --> y} (CE : Coequalizer f (ZeroArrow Z _ _)) :
    f · CoequalizerArrow CE = ZeroArrow Z x CE.
  Proof.
    rewrite <- (ZeroArrow_comp_left _ _ _ _ _ (CoequalizerArrow CE)).
    exact (CoequalizerEqAr CE).
  Qed.

  Lemma CoequalizerCokernel_isCokernel {x y : ob C} {f : x --> y}
        (CE : Coequalizer f (ZeroArrow Z _ _)) :
    isCokernel Z f (CoequalizerArrow CE) (CoequalizerCokernel_eq CE).
  Proof.
    use (make_isCokernel).
    intros w h H'.
    use unique_exists.
    - use CoequalizerOut.
      + exact h.
      + rewrite ZeroArrow_comp_left. exact H'.
    - use CoequalizerCommutes.
    - intros y0. apply hs.
    - intros y0 X. use CoequalizerOutsEq. rewrite CoequalizerCommutes. exact X.
  Qed.

  Definition CoequalizerCokernel {x y : ob C} {f : x --> y} (CE : Coequalizer f (ZeroArrow Z _ _)) :
    Cokernel Z f.
  Proof.
    use make_Cokernel.
    - exact CE.
    - exact (CoequalizerArrow CE).
    - exact (CoequalizerCokernel_eq CE).
    - exact (CoequalizerCokernel_isCokernel CE).
  Defined.

End cokernels_coequalizers.

Cokernels up to iso

Section cokernels_iso.

  Variable C : category.
  Let hs : has_homsets C := homset_property C.
  Variable Z : Zero C.

  Lemma Cokernel_up_to_iso_eq {x y z : C} (f : x --> y) (g : y --> z) (CK : Cokernel Z f)
        (h : z_iso CK z) (H : g = (CokernelArrow CK) · h) : f · g = ZeroArrow Z x z.
  Proof.
    induction CK as [t p]. induction t as [t' p']. induction p as [t'' p''].
    unfold isCoequalizer in p''.
    rewrite H.
    rewrite <- (ZeroArrow_comp_left _ _ _ _ _ h).
    rewrite assoc.
    apply cancel_postcomposition.
    apply CokernelCompZero.
  Qed.

  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 ((z_iso_inv_mor 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.

  Definition Cokernel_up_to_iso {x y z : C} (f : x --> y) (g : y --> z) (CK : Cokernel Z f)
             (h : z_iso CK z) (H : g = (CokernelArrow CK) · h) : Cokernel Z f :=
    make_Cokernel Z f g (Cokernel_up_to_iso_eq f g CK h H)
                (Cokernel_up_to_iso_isCokernel f g CK h H (Cokernel_up_to_iso_eq f g CK h H)).

  Definition Cokernel_up_to_iso2_eq {x y z : C} (f1 : x --> z) (f2 : y --> z) (h : z_iso y x)
             (H : h · f1 = f2) (CK : Cokernel Z f1) : f2 · CokernelArrow CK = ZeroArrow Z y CK.
  Proof.
    rewrite <- H. rewrite <- assoc. rewrite CokernelCompZero.
    apply ZeroArrow_comp_right.
  Qed.

  Definition Cokernel_up_to_iso2_isCoequalizer {x y z : C} (f1 : x --> z) (f2 : y --> z)
             (h : z_iso y x) (H : h · f1 = f2) (CK : Cokernel Z f1) :
    isCokernel Z f2 (CokernelArrow CK) (Cokernel_up_to_iso2_eq f1 f2 h H CK).
  Proof.
    use (make_isCokernel).
    intros w h0 H'.
    use unique_exists.
    - use CokernelOut.
      + exact h0.
      + rewrite <- H in H'. rewrite <- (ZeroArrow_comp_right _ _ _ _ _ h) in H'.
        rewrite <- assoc in H'. apply (pre_comp_with_z_iso_is_inj h) in H'.
        exact H'.
    - cbn. use CokernelCommutes.
    - intros y0. apply hs.
    - intros y0 X. cbn beta in X. use CokernelOutsEq. rewrite CokernelCommutes.
      exact X.
  Qed.

  Definition Cokernel_up_to_iso2 {x y z : C} (f1 : x --> z) (f2 : y --> z) (h : z_iso y x)
             (H : h · f1 = f2) (CK : Cokernel Z f1) : Cokernel Z f2 :=
    make_Cokernel Z f2 (CokernelArrow CK) (Cokernel_up_to_iso2_eq f1 f2 h H CK)
                (Cokernel_up_to_iso2_isCoequalizer f1 f2 h H CK).

End cokernels_iso.

Cokernel of epi · morphism

Introduction

Suppose E : x --> y is an Epi and f : y --> z is a morphism. Then cokernel of E · f is isomorphic to cokernel of f.
Section cokernels_epis.

  Variable C : category.
  Let hs : has_homsets C := homset_property C.
  Variable Z : Zero C.

  Local Lemma CokernelEpiComp_eq1 {x y z : C} (E : Epi C x y) (f : y --> z)
        (CK1 : Cokernel Z (E · f)) (CK2 : Cokernel Z f) :
    E · f · CokernelArrow CK2 = ZeroArrow Z x CK2.
  Proof.
    rewrite <- assoc. rewrite CokernelCompZero. apply ZeroArrow_comp_right.
  Qed.

  Definition CokernelEpiComp_mor1 {x y z : C} (E : Epi C x y) (f : y --> z)
             (CK1 : Cokernel Z (E · f)) (CK2 : Cokernel Z f) : C⟦CK1, CK2⟧ :=
    CokernelOut Z CK1 _ (CokernelArrow CK2) (CokernelEpiComp_eq1 E f CK1 CK2).

  Local Lemma CokernelEpiComp_eq2 {x y z : C} (E : Epi C x y) (f : y --> z)
        (CK1 : Cokernel Z (E · f)) (CK2 : Cokernel Z f) :
    f · CokernelArrow CK1 = ZeroArrow Z y CK1.
  Proof.
    use (EpiisEpi C E). rewrite assoc. rewrite ZeroArrow_comp_right. exact (CokernelCompZero Z CK1).
  Qed.

  Definition CokernelEpiComp_mor2 {x y z : C} (E : Epi C x y) (f : y --> z)
             (CK1 : Cokernel Z (E · f)) (CK2 : Cokernel Z f) : C⟦CK2, CK1⟧ :=
    CokernelOut Z CK2 _ (CokernelArrow CK1) (CokernelEpiComp_eq2 E f CK1 CK2).

  Lemma CokernelEpiComp1 {x y z : C} (E : Epi C x y) (f : y --> z)
        (CK1 : Cokernel Z (E · f)) (CK2 : Cokernel Z f) :
    is_iso (CokernelEpiComp_mor1 E f CK1 CK2).
  Proof.
    use is_iso_qinv.
    - exact (CokernelEpiComp_mor2 E f CK1 CK2).
    - split.
      + unfold CokernelEpiComp_mor1. unfold CokernelEpiComp_mor2.
        use CokernelOutsEq.
        rewrite assoc. rewrite CokernelCommutes. rewrite CokernelCommutes.
        apply pathsinv0. apply id_right.
      + unfold CokernelEpiComp_mor1. unfold CokernelEpiComp_mor2.
        use CokernelOutsEq.
        rewrite assoc. rewrite CokernelCommutes. rewrite CokernelCommutes.
        apply pathsinv0. apply id_right.
  Qed.

  Lemma CokernelEpiComp2 {x y z : C} (E : Epi C x y) (f : y --> z)
        (CK1 : Cokernel Z (E · f)) (CK2 : Cokernel Z f) :
    is_iso (CokernelEpiComp_mor2 E f CK1 CK2).
  Proof.
    use is_iso_qinv.
    - exact (CokernelEpiComp_mor1 E f CK1 CK2).
    - split.
      + unfold CokernelEpiComp_mor1. unfold CokernelEpiComp_mor2.
        use CokernelOutsEq.
        rewrite assoc. rewrite CokernelCommutes. rewrite CokernelCommutes.
        apply pathsinv0. apply id_right.
      + unfold CokernelEpiComp_mor1. unfold CokernelEpiComp_mor2.
        use CokernelOutsEq.
        rewrite assoc. rewrite CokernelCommutes. rewrite CokernelCommutes.
        apply pathsinv0. apply id_right.
  Qed.

  Local Lemma CokernelEpiComp_eq {x y z : C} (E : Epi C x y) (f : y --> z)
        (CK : Cokernel Z (E · f)) : f · CokernelArrow CK = ZeroArrow Z y CK.
  Proof.
    use (EpiisEpi C E). rewrite ZeroArrow_comp_right. rewrite assoc.
    use CokernelCompZero.
  Qed.

  Local Lemma CokernelEpiComp_isCoequalizer {x y z : C} (E : Epi C x y) (f : y --> z)
        (CK : Cokernel Z (E · f)) : isCokernel Z f (CokernelArrow CK) (CokernelEpiComp_eq E f CK).
  Proof.
    use make_isCokernel.
    - intros w h H'.
      use unique_exists.
      + use CokernelOut.
        × exact h.
        × rewrite <- (ZeroArrow_comp_right _ _ _ _ _ E). rewrite <- assoc.
          apply cancel_precomposition. exact H'.
      + cbn. rewrite CokernelCommutes. apply idpath.
      + intros y0. apply hs.
      + intros y0 X.
        apply pathsinv0. cbn in X.
        use (EpiisEpi C (make_Epi _ _ (CokernelArrowisEpi Z CK))). cbn.
        rewrite CokernelCommutes. apply pathsinv0. apply X.
  Qed.

  Definition CokernelEpiComp {x y z : C} (E : Epi C x y) (f : y --> z) (CK : Cokernel Z (E · f)) :
    Cokernel Z f.
  Proof.
    use make_Cokernel.
    - exact CK.
    - use CokernelArrow.
    - exact (CokernelEpiComp_eq E f CK).
    - exact (CokernelEpiComp_isCoequalizer E f CK).
  Defined.

End cokernels_epis.

CokernelOut of equal, not necessarily definitionally equal, morphisms is iso

Section cokernel_out_paths.

  Variable C : category.
  Let hs : has_homsets C := homset_property C.
  Variable Z : Zero C.

  Definition CokernelOutPaths_is_iso_mor {x y : C} {f f' : x --> y} (e : f = f')
             (CK1 : Cokernel Z f) (CK2 : Cokernel Z f') : CK1 --> CK2.
  Proof.
    induction e.
    use CokernelOut.
    - use CokernelArrow.
    - use CokernelCompZero.
  Defined.

  Lemma CokernelOutPaths_is_iso {x y : C} {f f' : x --> y} (e : f = f')
        (CK1 : Cokernel Z f) (CK2 : Cokernel Z f') : is_iso (CokernelOutPaths_is_iso_mor e CK1 CK2).
  Proof.
    induction e. apply CokernelsOut_is_iso.
  Qed.

  Local Lemma CokernelPath_eq {x y : C} {f f' : x --> y} (e : f = f') (CK : Cokernel Z f) :
    f' · CokernelArrow CK = ZeroArrow Z x CK.
  Proof.
    induction e. use CokernelCompZero.
  Qed.

  Local Lemma CokernelPath_isCokernel {x y : C} {f f' : x --> y} (e : f = f') (CK : Cokernel Z f) :
    isCokernel Z f' (CokernelArrow CK) (CokernelPath_eq e CK).
  Proof.
    induction e. use CokernelisCokernel.
  Qed.

Constructs a cokernel of f' from a cokernel of f in a natural way
  Definition CokernelPath {x y : C} {f f' : x --> y} (e : f = f') (CK : Cokernel Z f) :
    Cokernel Z f'.
  Proof.
    use make_Cokernel.
    - exact CK.
    - use CokernelArrow.
    - exact (CokernelPath_eq e CK).
    - exact (CokernelPath_isCokernel e CK).
  Defined.

End cokernel_out_paths.