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 = Univalent.isoβpath ccat (β₯-unique x1 x2) i β₯-contractible ccat x1 x2 i .hasβ₯ ob = is-propβpathp (Ξ» i β is-contr-is-prop {A = Hom (Univalent.isoβpath ccat (β₯-unique x1 x2) i) _}) (x1 .hasβ₯ ob) (x2 .hasβ₯ ob) i