{-# 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
  }