# Initial Object

We define initial and terminal objects, which we shall use for describing algebras and initial algebras.

(Definition) Let `𝒞` be a category. An object `0` is the initial object of `𝒞` if, for all objects `a`, there is a unique morphism `0 → a`.

(Definition) Let `𝒞` be a category. An object `1` is the terminal object of `𝒞` if, for all objects `a`, there is a unique morphism `a → 1`.

(Lemma) Initial and terminal objects are unique up to isomorphism.

(Proof) Let 𝒞 be a category with initial objects 0 and 0′. There are unique morphisms `00′ ∶ 0 → 0′` and `0′0 ∶ 0′ → 0`, and `00 = id0` and `0′ 0′ = id0′`. Hence, `0′0 ∘ 00′ = id0` and `00′ ∘ 0′0 = id0′`. That is, 0 is unique up to isomorphism. Similarly, let `𝒞` be a category with terminal objects 1 and 1′. There are unique morphisms `11′ ∶ 1′ → 1` and `1′1 ∶ 1 → 1′`, and `11 = id1` and `1′1′ = id1′`. Hence, `11′ ∘ 1′1 = id1` and `1′1 ∘ 11′ = id1′`. That is, 1 is unique up to isomorphism.

In Hask, Void (the empty or uninhabited type) is the initial object, and unit or `()` type is the terminal object.

In Set, the elements of a set 𝐴 can be considered as functions from a terminal object, that is, any singleton set, to 𝐴. More specifically, if 𝑥 ∈ 𝐴 and 1 is a terminal object, then 𝑥 can be considered as a function 𝑥 ∶ 1 → 𝐴 which assigns 𝑥 to the element of 1.