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