I am working on Category Theory for Programmers book.
Here in the book I find the "<=" relationship as an example of category: it respects the identity relationship (a <= a) and it is composable (a <= b, b <= c -> a <= c).
What is not clear to me is the analogy between morphisms and functions, as mentioned in the book at page 3: a function cannot implement the order category, as it cannot return any value <= of a given one, so… what is the relation between morphisms and functions? It seems to be that morphisms are connections between types, whereas functions definitions are connections between values, so the latter sounds to me as a special implementation of the former.
This would be in contrast with all the examples of identity functions I saw out there, though, as an identity function would map a type with the same type, not a value with the same value, so, for instance, f x = x + 1 would be a correct "arrow" from and to the same type, which is evidently not true.
On the other hand, though, I see such category representations:
Here A is a type or is an object?
Best Answer
I don't quite understand what you're confused about, and in particular I don't quite understand what you mean by "a function cannot implement the order category," so I'll just say some things I hope are relevant.
Morphisms don't start out as having any particular interpretation in terms of functions. The bare category axioms just give you a bunch of objects and arrows and axioms for how arrows should compose, and those axioms are satisfied by any partial order $\le$, and that's it. When starting out I think the least confusing way to think about categories in this "bare" way is to think of them as directed graphs equipped with a composition operation on edges.
On the other hand, every category $C$ has a Yoneda embedding $C \to [C^{op}, \text{Set}]$, which gives us a distinguished interpretation of morphisms $f : x \to y$ as functions $f : \text{Hom}(a, x) \to \text{Hom}(a, y)$ on generalized points, where a generalized point of $x$ is just any morphism $a \to x$ whatsoever. This lets us interpret the morphisms $x \le y$ in a partial order as functions (necessarily unique) from the downsets $\{ a : a \le x \}$ to the downsets $\{ a : a \le y \}$, namely the unique function sending $a$ to $a$.
Objects also don't start out as having any particular interpretation in terms of types. Type theory is a particular way of looking at categories, or a particular way of generating them, and it's not the only one. In the standard categorical semantics for type theories, objects are (interpreted as) types $A$ and morphisms $f : A \to B$ are (interpreted as) functions with input type $A$ and output type $B$. If a category has a terminal object $1$ (which can be interpreted as a unit type) then morphisms $1 \to A$ can be interpreted as terms of type $A$, and a morphism $f : A \to B$ then induces a genuine function $\text{Hom}(1, A) \to \text{Hom}(1, B)$ sending terms of type $A$ to terms of type $B$. There are often not enough "points" (functions $1 \to A$) to make this an interesting operation in many categories, though; for example, in posets $1$, if it exists, is a maximal element, so $\text{Hom}(1, A)$ is empty unless $A$ is also maximal.