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

# Initial objectsπ

An object $\bot$ of a category $\mathcal{C}$ is said to be **initial** if there exists a *unique* map to any other object:

is-initial : Ob β Type _ is-initial ob = β x β is-contr (Hom ob x) record Initial : Type (o β h) where field bot : Ob hasβ₯ : is-initial bot

We refer to the centre of contraction as Β‘. Since it inhabits a contractible type, it is unique.

Β‘ : β {x} β Hom bot x Β‘ = hasβ₯ _ .centre Β‘-unique : β {x} (h : Hom bot x) β Β‘ β‘ h Β‘-unique = hasβ₯ _ .paths Β‘-uniqueβ : β {x} (f g : Hom bot x) β f β‘ g Β‘-uniqueβ = is-contrβis-prop (hasβ₯ _) open Initial

## Intuitionπ

The intuition here is that we ought to think about an initial object as having βthe least amount of structure possible,β insofar that it can be mapped *into* any other object. For the category of `Sets`

, this is the empty set; there is no required structure beyond βbeing a set,β so the empty set sufficies.

In more structured categories, the situation becomes a bit more interesting. Once our category has enough structure that we canβt build maps from a totally trivial thing, the initial object begins to behave like a notion of **Syntax** for our category. The idea here is that we have a *unique* means of interpreting our syntax into any other object, which is exhibited by the universal map Β‘

## Uniquenessπ

One important fact about initial objects is that they are **unique** up to isomorphism:

β₯-unique : (i iβ² : Initial) β bot i β bot iβ² β₯-unique i iβ² = make-iso (Β‘ i) (Β‘ iβ²) (Β‘-uniqueβ iβ² _ _) (Β‘-uniqueβ i _ _)

Additionally, if $C$ is a category, then the space of initial objects is a proposition:

β₯-contractible : is-category C β is-prop Initial β₯-contractible ccat x1 x2 i .bot = isoβpath C ccat (β₯-unique x1 x2) i β₯-contractible ccat x1 x2 i .hasβ₯ ob = is-propβpathp (Ξ» i β is-contr-is-prop {A = Hom (isoβpath C ccat (β₯-unique x1 x2) i) _}) (x1 .hasβ₯ ob) (x2 .hasβ₯ ob) i