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'.
  Show proof.
    assert (e : H = H') by apply hs.
    induction e. exact isC.

  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')).
  Show proof.
    intros y0 H. apply (base_paths _ _ ((pr2 (H2 w h H')) (tpair _ y0 H))).

  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.
  Show 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))).

  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'))).
  Show proof.
    exact (base_paths _ _ (pr2 (isCK w h H') (tpair _ φ H''))).

  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.
  Show 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).

  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.
  Show proof.
    use CokernelOutsEq. rewrite CokernelCommutes. rewrite assoc. rewrite CokernelCommutes.
    apply idpath.

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).
  Show proof.
    exists (identity CK).
    apply id_right.

  Lemma CokernelEndo_is_identity {x y : C} {f : x --> y} {CK : Cokernel f} (φ : C⟦CK, CK⟧)
        (H : (CokernelArrow CK) · φ = CokernelArrow CK) : identity CK = φ.
  Show 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).

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

  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).
  Show 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.

  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)).
  Show 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.

  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)).
  Show 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.

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

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)).
  Show 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.

  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).
  Show proof.
    unfold isEpi.
    intros z0 g0 h X.
    use CokernelOutsEq.
    exact X.

  Lemma CokernelsOut_is_iso {x y : C} {f : x --> y} (CK1 CK2 : Cokernel f) :
    is_iso (CokernelOut CK1 CK2 (CokernelArrow CK2) (CokernelCompZero CK2)).
  Show 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.

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.
  Show proof.
    rewrite ZeroArrow_comp_left. use CokernelCompZero.

  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).
  Show 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.

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

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.
  Show proof.
    rewrite <- (ZeroArrow_comp_left _ _ _ _ _ (CoequalizerArrow CE)).
    exact (CoequalizerEqAr CE).

  Lemma CoequalizerCokernel_isCokernel {x y : ob C} {f : x --> y}
        (CE : Coequalizer f (ZeroArrow Z _ _)) :
    isCokernel Z f (CoequalizerArrow CE) (CoequalizerCokernel_eq CE).
  Show 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.

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

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.
  Show 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.

  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''.
  Show 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.

  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.
  Show proof.
    rewrite <- H. rewrite <- assoc. rewrite CokernelCompZero.
    apply ZeroArrow_comp_right.

  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).
  Show 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.

  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.
  Show proof.
    rewrite <- assoc. rewrite CokernelCompZero. apply ZeroArrow_comp_right.

  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.
  Show proof.
    use (EpiisEpi C E). rewrite assoc. rewrite ZeroArrow_comp_right. exact (CokernelCompZero Z CK1).

  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).
  Show 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.

  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).
  Show 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.

  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.
  Show proof.
    use (EpiisEpi C E). rewrite ZeroArrow_comp_right. rewrite assoc.
    use CokernelCompZero.

  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).
  Show 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.

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

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.
  Show proof.
    induction e.
    use CokernelOut.
    - use CokernelArrow.
    - use CokernelCompZero.

  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).
  Show proof.
    induction e. apply CokernelsOut_is_iso.

  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.
  Show proof.
    induction e. use CokernelCompZero.

  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).
  Show proof.
    induction e. use CokernelisCokernel.

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'.
  Show proof.
    use make_Cokernel.
    - exact CK.
    - use CokernelArrow.
    - exact (CokernelPath_eq e CK).
    - exact (CokernelPath_isCokernel e CK).

End cokernel_out_paths.