Processing math: 100%

Initial object

Object

context C … category
definiendum I:ObC
for all X:ObC
postulate !i. i:C[I,X]

Discussion

Alternative definitions

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

Reference

Wikipedia: Initial and terminal objects

Parents

Context

Categories

Requirements

Category theory

Element of

Initial morphism

Terminal object