{-# OPTIONS --without-K --safe #-}
open import Categories.Category
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)