open import Cat.Univalent open import Cat.Prelude module Cat.Diagram.Zero {o h} (C : Precategory o h) where open import Cat.Diagram.Initial C open import Cat.Diagram.Terminal C

# Zero Objectsπ

In some categories, Initial
and Terminal objects coincide. When this occurs,
we call the object a **zero object**.

record is-zero (ob : Ob) : Type (o β h) where field has-is-initial : is-initial ob has-is-terminal : is-terminal ob record Zero : Type (o β h) where field β : Ob has-is-zero : is-zero β open is-zero has-is-zero public terminal : Terminal terminal = record { top = β ; hasβ€ = has-is-terminal } initial : Initial initial = record { bot = β ; hasβ₯ = has-is-initial } open Terminal terminal public hiding (top) open Initial initial public hiding (bot)

A curious fact about zero objects is that their existence implies that every hom set is inhabited!

zeroβ : β {x y} β Hom x y zeroβ = Β‘ β ! zero-βl : β {x y z} β (f : Hom y z) β f β zeroβ {x} {y} β‘ zeroβ zero-βl f = pulll (sym (Β‘-unique (f β Β‘))) zero-βr : β {x y z} β (f : Hom x y) β zeroβ {y} {z} β f β‘ zeroβ zero-βr f = pullr (sym (!-unique (! β f)))

## Intuitionπ

Most categories that have zero objects have enough structure to rule
out *totally* trivial structures like the empty set, but not
enough structure to cause the initial and terminal objects to
βseparateβ. The canonical example here is the category of groups: the
unit rules out a completely trivial group, yet thereβs nothing else that
would require the initial object to have any more structure.

Another point of interest is that any category with zero objects is canonically enriched in pointed sets: the zeroβ morphism from earlier acts as the designated basepoint for each of the hom sets.