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

open import Categories.Category

-- a zero object is both terminal and initial.
module Categories.Object.Zero {o  e} (C : Category o  e) where

open import Level

open import Categories.Object.Terminal C
open import Categories.Object.Initial C

open import Categories.Morphism C
open import Categories.Morphism.Reasoning C

open Category C
open HomReasoning

record IsZero (Z : Obj) : Set (o    e) where
  field
    isInitial : IsInitial Z
    isTerminal : IsTerminal Z

  open IsInitial isInitial public
    renaming
    ( ! to ¡
    ; !-unique to ¡-unique
    ; !-unique₂ to ¡-unique₂
    )
  open IsTerminal isTerminal public

  zero⇒ :  {A B : Obj}  A  B
  zero⇒ = ¡  !

  zero-∘ˡ :  {X Y Z}  (f : Y  Z)  f  zero⇒ {X}  zero⇒
  zero-∘ˡ f = pullˡ ( (¡-unique (f  ¡)))

  zero-∘ʳ :  {X Y Z}  (f : X  Y)  zero⇒ {Y} {Z}  f  zero⇒
  zero-∘ʳ f = pullʳ ( (!-unique (!  f)))

record Zero : Set (o    e) where
  field
    𝟘 : Obj
    isZero : IsZero 𝟘

  open IsZero isZero public

  terminal : Terminal
  terminal = record { ⊤-is-terminal = isTerminal }

  initial : Initial
  initial = record { ⊥-is-initial = isInitial }

open Zero

¡-Mono :  {A} {z : Zero}  Mono (¡ z {A})
¡-Mono {z = z} = from-⊤-is-Mono {t = terminal z} (¡ z)

!-Epi :  {A} {z : Zero}  Epi (! z {A})
!-Epi {z = z} = to-⊥-is-Epi {i = initial z} (! z)