module Cat.Diagram.Initial {o h} (C : Precategory o h) where
Initial objectsπ
An object of a category 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 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