{-# OPTIONS --without-K --safe #-}

open import Categories.Category
open import Categories.Object.Zero

-- Cokernels of morphisms.
-- https://ncatlab.org/nlab/show/cokernel
module Categories.Object.Cokernel {o  e} {𝒞 : Category o  e} (𝟎 : Zero 𝒞) where

open import Level

open import Categories.Morphism 𝒞
open import Categories.Morphism.Reasoning 𝒞
  hiding (glue)

open Category 𝒞
open Zero 𝟎

open HomReasoning

private
  variable
    A B X : Obj
    f h i j k : A  B

record IsCokernel {A B K} (f : A  B) (k : B  K) : Set (o    e) where
  field
    commute   : k  f  zero⇒
    universal :  {X} {h : B  X}  h  f  zero⇒  K  X
    factors   :  {eq : h  f  zero⇒}  h  universal eq  k
    unique    :  {eq : h  f  zero⇒}  h  i  k  i  universal eq

  universal-resp-≈ :  {eq : h  f  zero⇒} {eq′ : i  f  zero⇒} 
    h  i  universal eq  universal eq′
  universal-resp-≈ h≈i = unique ( h≈i  factors)

  universal-∘ : h  k  f  zero⇒
  universal-∘ {h = h} = begin
    h  k  f ≈⟨ refl⟩∘⟨ commute 
    h  zero⇒ ≈⟨ zero-∘ˡ h 
    zero⇒     

record Cokernel {A B} (f : A  B) : Set (o    e) where
  field
    {cokernel} : Obj
    cokernel⇒  : B  cokernel
    isCokernel : IsCokernel f cokernel⇒

  open IsCokernel isCokernel public

IsCokernel⇒Cokernel : IsCokernel f k  Cokernel f
IsCokernel⇒Cokernel {k = k} isCokernel = record
  { cokernel⇒ = k
  ; isCokernel = isCokernel
  }