Categorías como funciones

Question

Estoy trabajando en el libro Teoría de categorías para programadores .

Aquí en el libro encuentro la relación "<=" como ejemplo de categoría: respeta la relación de identidad ( a <= a) y es componible ( a <= b, b <= c -> a <= c).

Lo que no me queda claro es la analogía entre morfismos y funciones, como se menciona en el libro en la página 3: una función no puede implementar la categoría de orden, ya que no puede devolver ningún valor <= de uno dado, entonces ... lo que es la relación entre morfismos y funciones? Parece ser que los morfismos son conexiones entre tipos, mientras que las definiciones de funciones son conexiones entre valores, por lo que el último me suena como una implementación especial del primero.

Sin embargo, esto contrastaría con todos los ejemplos de funciones de identidad que vi, ya que una función de identidad mapearía un tipo con el mismo tipo, no un valor con el mismo valor, por lo que, por ejemplo, f x = x + 1sería un correcto " flecha "desde y hacia el mismo tipo, lo que evidentemente no es cierto.

Sin embargo, por otro lado, veo tales representaciones de categorías:

¿Aquí A es un tipo o es un objeto?

Answer 1

No entiendo muy bien por qué estás confundido y, en particular, no entiendo muy bien lo que quieres decir con "una función no puede implementar la categoría de orden", así que solo diré algunas cosas que espero sean relevantes.

1. Los morfismos no comienzan teniendo una interpretación particular en términos de funciones. Los axiomas de categoría básica solo le dan un montón de objetos y flechas y axiomas sobre cómo deben componerse las flechas, y esos axiomas se satisfacen con cualquier orden parcial $\le$, y eso es. Al comenzar, creo que la forma menos confusa de pensar en las categorías de esta manera "desnuda" es pensar en ellas como gráficos dirigidos equipados con una operación de composición en los bordes.

2. Por otro lado, cada categoría $C$tiene una incrustación de Yoneda $C \to [C^{op}, \text{Set}]$, lo que nos da una interpretación distinguida de los morfismos $f : x \to y$ como funciones $f : \text{Hom}(a, x) \to \text{Hom}(a, y)$en puntos generalizados , donde un punto generalizado de$x$ es cualquier morfismo $a \to x$lo que. Esto nos permite interpretar los morfismos$x \le y$en un orden parcial como funciones (necesariamente únicas) de los downsets $\{ a : a \le x \}$ a los downsets $\{ a : a \le y \}$, es decir, la función única que envía $a$ a $a$.

3. Los objetos tampoco comienzan teniendo una interpretación particular en términos de tipos. La teoría de tipos es una forma particular de ver las categorías, o una forma particular de generarlas, y no es la única. En la semántica categórica estándar para las teorías de tipos, los objetos son (interpretados como) tipos$A$ y morfismos $f : A \to B$ son (interpretadas como) funciones con tipo de entrada $A$ y tipo de salida $B$. Si una categoría tiene un objeto terminal $1$ (que se puede interpretar como un tipo de unidad) luego morfismos $1 \to A$ se puede interpretar como términos de tipo $A$y un morfismo $f : A \to B$ luego induce una función genuina $\text{Hom}(1, A) \to \text{Hom}(1, B)$ envío de términos de tipo $A$ a términos de tipo $B$. A menudo no hay suficientes "puntos" (funciones$1 \to A$) para hacer de esta una operación interesante en muchas categorías; por ejemplo, en posets$1$, si existe, es un elemento máximo , entonces$\text{Hom}(1, A)$ está vacío a menos que $A$ también es máxima.