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

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

-- Normal Mono and Epimorphisms
-- https://ncatlab.org/nlab/show/normal+monomorphism
module Categories.Morphism.Normal {o β„“ e} (π’ž : Category o β„“ e) (π’ž-Zero : Zero π’ž) where

open import Level

open import Categories.Object.Kernel π’ž-Zero
open import Categories.Object.Kernel.Properties π’ž-Zero
open import Categories.Morphism π’ž

open Category π’ž

record IsNormalMonomorphism {A K : Obj} (k : K β‡’ A) : Set (o βŠ” β„“ βŠ” e) where
  field
    {B} : Obj
    arr : A β‡’ B
    isKernel : IsKernel k arr

  open IsKernel isKernel public

  mono : Mono k
  mono = Kernel-Mono (IsKernel⇒Kernel isKernel)

record NormalMonomorphism (K A : Obj) : Set (o βŠ” β„“ βŠ” e) where
  field
    mor : K β‡’ A
    isNormalMonomorphism : IsNormalMonomorphism mor

  open IsNormalMonomorphism isNormalMonomorphism public