Cfrgtkky

(I'm using Haskell syntax)

So I have an initial object, which I call $text{Void}$. The prerequisite for an inital object is $forall X in text{Hask.} exists ! f : text{Void} to X$. But how is that true?
Can't I just say:

f :: Void -> Int

f _ = 1



f' :: Void -> Int

f _ = 2



(...)

The same applies to Set, with a set $I in text{Set}$ such that $forall X in text{Set}. exists! f : I rightarrow X$, where $I = emptyset$::

$$
f: emptyset rightarrow mathbb{N} \
f(x) = 1 \
f': emptyset rightarrow mathbb{N} \
f'(x) = 2 \
...
$$

Of course I can't call any of them, because the prerequisites of having an element of type Void will never hold true, but still, I can create as many functions as I want.

And if pattern matching is illegal, then how can I even create a single function?

f'' :: Void -> a

-- how is this ok?

I'm not very familiar with Haskell, but let me give an answer from category theory; I believe that this should transfer over to a large extent.

The function "$f(x)=2$" isn't really a function from $emptyset$ - rather, its restriction to $emptyset$ is. And the restrictions of $xmapsto 2$ and $xmapsto 1$ to $emptyset$ are the same.

This becomes clear when we think of functions set-theoretically: a function from $A$ to $B$ is a susbet $f$ of $Atimes B$ such that for each $ain A$ there is exactly one $bin B$ with $(a, b)in f$.

Now of course, when working with Haskell the phrase "thinking of functions set-theoretically" is probably a bit cringe-inducing; but it nonetheless has its place here. In the category Set, a morphism from $A$ to $B$ is a triple $(f, A, B)$ where $fsubseteq Atimes B$ is a set-theoretic function from $A$ to $B$.

The key here is that, in both category theory (or rather, the specific category Set - there are other "categories of sets") and set theory, we identify it with its graph, not its intensional definition; so "map everything to $2$" and "map everything to $1$," while intensionally different, yield the same set-theoretic function.

For $mathsf{Set}$, the morphism $0 to X$ is simply the empty function (i.e. view a function as a subset of the cartesian product, choose the empty subset).

I do not know if this is ideal, but you can express this in Haskell as:

data Void



i :: Void -> a

i x = case x of {}

You need to run GHC with -XEmptyCase.

I think what confused me when I wrote the question is the Haskell syntax.
You got to remember that the _ character is just a syntactic sugar. It means "for all remaining cases, assign that value". If I had realized that, I probably wouldn't have posed that question. Because "technically" it should look like this:

f :: Void -> Int

Because there is not even a first case. Saying "all remaining cases", although there are zero cases is like saying, "Every person in this room is a doctor.", where the room is empty. There is still no doctor in the room.

Also another thing that is important to remember is that in a mathematical sense, functions are equal, if they produce the same output for every possible output. This is definitely true of the functions I've written above:

f :: Void -> Int

f _ = 1



f' :: Void -> Int

f _ = 2

They both give the same output for all imaginable input (which is none).

Another way to think about it is visually in the category of $Set$. I've drawn a quick picture for that purpose:

Yet another fun fact is that you can use $n^k$ to calculate the number of morphisms of type $K rightarrow N, |K| = k, |N| = n$. And as we now, $n^0$ is 1 for all $n$.