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

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

-- Kernels of morphisms.
-- https://ncatlab.org/nlab/show/kernel
module Categories.Object.Kernel {o  e} {𝒞 : Category o  e} (zero : Zero 𝒞) where

open import Level using (_⊔_)

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

open Category 𝒞
open Zero zero

open HomReasoning

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

-- Note: We could define Kernels directly as equalizers or as pullbacks, but it seems somewhat
-- cleaner to just define them "as is" to avoid mucking about with extra morphisms that can
-- get in the way. For example, if we defined them as 'Pullback f !' then our 'p₂' projection
-- would _always_ be trivially equal to '¡ : K ⇒ zero'.

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

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

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

record Kernel {A B} (f : A  B) : Set (o    e) where
  field
     {kernel} : Obj
     kernel⇒ : kernel  A
     isKernel : IsKernel kernel⇒ f

  open IsKernel isKernel public

IsKernel⇒Kernel : IsKernel k f  Kernel f
IsKernel⇒Kernel {k = k} isKernel = record
  { kernel⇒ = k
  ; isKernel = isKernel
  }