What is the proof that there is only one homomorphism from an initial object to another object?

  • $\begingroup$ Oops, sorry. I completely misunderstood your question, I suppose! $\endgroup$ Aug 21, 2010 at 21:03
  • 1
    $\begingroup$ en.wikipedia.org/wiki/Initial_and_terminal_objects $\endgroup$ Aug 21, 2010 at 23:02
  • $\begingroup$ Small correction: "morphism" instead of "homomorphism" is used in the context of category theory. $\endgroup$
    – beroal
    Oct 25, 2010 at 19:08

2 Answers 2


To add on top of finrod's answer: while the existence of an initial object guarantees the uniqueness of the aforesaid morphism, the initial object's existence is not guaranteed.

As you asked this question under the functional programming tag, perhaps you meant to ask how to establish the existence of initial algebras for a given algebraic type in a functional programming language.

The existence of an initial object is not entirely trivial, but if you know some domain theory then the proof is very similar to the least fixed point theorem for continuous functions over directed CPOs.

The canonical reference eludes me right now, but brief Googling/Wikipedia dig up Abramsky's and Jung's chapter on Domain Theory (section 5, this case is the example in 5.1.3) in the Handbook of Logic in CS.


As far as I remember (and my copy of Pierce's Basic Category Theory for Computer Scientists confirms this), the initial object is defined as an object with exactly one arrow to each object in the category.

  • $\begingroup$ Exactly. If there isn't exactly one morphism from the initial object to all objects, then it isn't initial :) $\endgroup$ Oct 20, 2010 at 8:24

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.