context | C … category |
definiendum | I:ObC |
for all | X:ObC |
postulate | ∃!i. i:C[I,X] |
The initial object of C can be characterized by the initial morphism ⟨I,id∙⟩ from ∙:Ob1 to the (unique) functor U mapping to the discrete category 1, which only has a single object. Because then U(g)=f is trivially true for all g:MorC and f:Mor1 (the latter is necessarily the identity), the initial morphisms definition reduces to the statement that C[I,X] has only one term:
∀X:ObC. ∃!(g:C[I,X]). true
Wikipedia: Initial and terminal objects