module Cat.Diagram.Initial where

# Initial objectsπ

An object
$β₯$
of a category
$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:

β₯-is-prop : is-category C β is-prop Initial β₯-is-prop ccat x1 x2 i .bot = Univalent.isoβpath ccat (β₯-unique x1 x2) i β₯-is-prop 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

## Strictnessπ

An initial object is said to be *strict*
if every morphism into it is an *iso*morphism. This is a
categorical generalization of the fact that if one can write a function
$Xββ₯$
then
$X$
must itself be empty.

This is an instance of the more general notion of van Kampen colimits.

is-strict-initial : Initial β Type _ is-strict-initial i = β x β (f : Hom x (i .bot)) β is-invertible f record Strict-initial : Type (o β h) where field initial : Initial has-is-strict : is-strict-initial initial

Strictness is a property of, not structure on, an initial object.

is-strict-initial-is-prop : β i β is-prop (is-strict-initial i) is-strict-initial-is-prop i = hlevel 1

module _ {o h} {C : Precategory o h} where open Cat.Morphism C private unquoteDecl eqv = declare-record-iso eqv (quote Initial) instance Extensional-Initial : β {βr} β β¦ sa : Extensional Ob βr β¦ β Extensional (Initial C) βr Extensional-Initial β¦ sa β¦ = embeddingβextensional (IsoβEmbedding eqv βemb (fst , Subset-proj-embedding Ξ» _ β hlevel 1)) sa