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