Bartosz Milewski, in the section Terminal Object of Chapter 5 underlines the following
Notice that in this example the uniqueness condition is crucial, because there are other sets (actually, all of them, except for the empty set) that have incoming morphisms from every set. For instance, there is a Boolean-valued function (a predicate) defined for every type:
yes :: a -> Bool yes _ = True
But
Bool
is not a terminal object. There is at least one moreBool
-valued function from every type:no :: a -> Bool no _ = False
Insisting on uniqueness gives us just the right precision to narrow down the definition of the terminal object to just one type.
And all this come after the section Initial Object, where a similar observation is not made.
Therefore I have the feeling that I might be missing a key difference between initial and terminal objects.
From my understanding the uniqueness is crucial also for initial objects, because I could observe that there are other sets (actually, all of them) that have an outgoing morphisms to every set (except the empty set), but there would be in general more than one such a morphism (except for the one going to ()
).
So my question is: is there any difference between initial and terminal objects, beside the direction of the arrows that connect them to the other objects, that Bartosz is probably trying to underline with the quoted text?
I know that question like What does the author mean? can be a bit ill posed, as we are not in his mind, but I guess who knows category theory can throw at least some plausible hypothesis.
that have an outgoing morphisms to every set (except the empty set)
That's the key part. The requirement is that there be outgoing morphisms to every set full stop. The existance of one set where this breaks down is enough to undermine it. That's why, indeed, the initial object in Set
is already well-defined without even requiring uniqueness: the empty set is the only set that has an outgoing arrow to the empty set.
Meanwhile, every non-empty set has incoming arrows from truely every set including the empty one, but only for one-element sets is this arrow unique.