open import Cat.Prelude

import Cat.Morphism

module Cat.Diagram.Initial where

module _ {o h} (C : Precategory o h) where
open Cat.Morphism C


# 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:

  β₯-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 isomorphism. This is a categorical generalization of the fact that if one can write a function then 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