Dear all, Before asking what the morphisms 0 -> A are, one should probably fix a category. This involves choosing a programming language and a notion of equivalence for programs, and both choices impact on the existence of an initial object. 1) A first possibility consists of choosing a programming language and considering the category where: - objects are types (possibly a single one for untyped languages such as Scheme), - morphisms A -> B are programs of type B with one variable of type A (or variants such as the one proposed by Mike Schulman), considered equivalent up to observational equivalence. Observational equivalence might mean a lot of different things. Let us here put M ~ N : A -> B when for all P : B -> Bool and Q : 1 -> A, PMQ evaluates to true iff PNQ evaluates to true. (If your programming language allows infinite loops, you may replace Bool with 1 and observe termination.) Then, if your programming language has an empty type A, i.e., one without any program 1 -> A, it is initial because M ~ N vacuously holds. An example such programming language is Agda (using an inductive type with no constructor). 2) However, in Haskell, you may define an inhabitant of all types by typing the recursive definition bot = bot . You may also define functions: f x = True and g x = False having all types A -> Bool, which are not equivalent because f bot evaluates to True while g bot evaluates to False. 3) But there are other possible notions of equivalence! For example, one may consider only beta, eta, ... equivalence. Then, even with an empty type A, the functions f x = True and g x = False are different, hence A is not initial. 4) As a final remark, even in a consistent setting like Agda, functions from the empty type are frequently applied (in an open context), typically the canonical function (A * not A) -> B, which looks like f (x, y) = !(y(x)), where !M = match M with {} -- case analysis on zero constructors. Pierre Hyvernat and Tom Hirschowitz --