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

CC BY-SA 2.5
2010-10-20T08:24:57.183Z
Exactly. If there isn't exactly one morphism from the initial object to all objects, then it isn't initial :)
wren romano
CC BY-SA 2.5
2010-08-21T20:36:04.130Z
2010-08-21T20:36:04.130Z
finrod
<p>To add on top of <a href="https://cstheory.stackexchange.com/questions/372/proof-of-a-unique-homomorphism-from-an-initial-object/374#374">finrod's answer</a>: while the existence of an initial object guarantees the uniqueness of the aforesaid morphism, the initial object's <strong>existence</strong> is not guaranteed.</p>

<p>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.</p>

<p>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.</p>

<p>The canonical reference eludes me right now, but brief Googling/Wikipedia dig up Abramsky's and Jung's chapter on <a href="http://www.cs.bham.ac.uk/~axj/pub/papers/handy1.pdf" rel="nofollow noreferrer">Domain Theory</a> (section 5, this case is the example in 5.1.3) in the Handbook of Logic in CS.  </p>

CC BY-SA 2.5
2010-08-21T21:23:11.247Z
2010-08-22T19:13:13.633Z
2017-04-13T12:32:28.117Z
Ohad Kammar
<p>What is the proof that there is only one homomorphism from an initial object to another object?</p>

CC BY-SA 2.5
2010-08-21T21:03:59.050Z
Oops, sorry. I completely misunderstood your question, I suppose!
Daniel Apon
CC BY-SA 2.5
2010-08-21T23:02:40.680Z
http://en.wikipedia.org/wiki/Initial_and_terminal_objects
Dave Clarke
CC BY-SA 2.5
2010-10-25T19:08:17.540Z
Small correction: "morphism" instead of "homomorphism" is used in the context of category theory.
beroal
<functional-programming><algebra><ct.category-theory>
Proof of a unique homomorphism from an initial object
Jason Reich
# Proof of a unique homomorphism from an initial object

(Asked by: username_0 on 2010-08-21)

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

**Tags:** functional-programming, algebra, ct.category-theory
> **Comments:**
> **username_1**: Oops, sorry. I completely misunderstood your question, I suppose!  
> **username_2**: http://en.wikipedia.org/wiki/Initial_and_terminal_objects  
> **username_3**: Small correction: "morphism" instead of "homomorphism" is used in the context of category theory.  

---

## 2 answers

### Answer by username_6 on 2010-08-21. Score: 6 | Accepted answer

To add on top of [finrod's answer](https://cstheory.stackexchange.com/questions/372/proof-of-a-unique-homomorphism-from-an-initial-object/374#374): 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](http://www.cs.bham.ac.uk/~axj/pub/papers/handy1.pdf) (section 5, this case is the example in 5.1.3) in the Handbook of Logic in CS.


---

### Answer by username_4 on 2010-08-21. Score: 14

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.

> **Comments:**
> **username_5**: Exactly. If there isn't exactly one morphism from the initial object to all objects, then it isn't initial :)  

---

