Categorie come funzioni

Question

Sto lavorando al libro Teoria delle categorie per programmatori .

Qui nel libro trovo la relazione "<=" come esempio di categoria: rispetta la relazione di identità ( a <= a) ed è componibile ( a <= b, b <= c -> a <= c).

Quello che non mi è chiaro è l'analogia tra morfismi e funzioni, come accennato nel libro a pagina 3: una funzione non può implementare la categoria dell'ordine, in quanto non può restituire alcun valore <= di una data, quindi ... il rapporto tra morfismi e funzioni? Sembra che i morfismi siano connessioni tra tipi, mentre le definizioni di funzioni sono connessioni tra valori, quindi quest'ultima mi sembra un'implementazione speciale del primo.

Ciò sarebbe in contrasto con tutti gli esempi di funzioni di identità che ho visto là fuori, tuttavia, poiché una funzione di identità mapperebbe un tipo con lo stesso tipo, non un valore con lo stesso valore, quindi, ad esempio, f x = x + 1sarebbe corretto " freccia "da e verso lo stesso tipo, il che evidentemente non è vero.

D'altra parte, però, vedo tali rappresentazioni di categoria:

Qui A è un tipo o è un oggetto?

Answer 1

Non capisco bene di cosa sei confuso, e in particolare non capisco cosa intendi per "una funzione non può implementare la categoria dell'ordine", quindi dirò solo alcune cose che spero siano rilevanti.

1. I morfismi non iniziano con una particolare interpretazione in termini di funzioni. Gli assiomi della categoria nuda ti danno solo un mucchio di oggetti e frecce e assiomi su come le frecce dovrebbero comporsi, e quegli assiomi sono soddisfatti da qualsiasi ordine parziale $\le$e questo è tutto. All'inizio penso che il modo meno confuso di pensare alle categorie in questo modo "nudo" sia pensarle come grafici orientati dotati di un'operazione di composizione sui bordi.

2. D'altra parte, ogni categoria $C$ha un'incorporazione Yoneda $C \to [C^{op}, \text{Set}]$, che ci fornisce una distinta interpretazione dei morfismi $f : x \to y$ come funzioni $f : \text{Hom}(a, x) \to \text{Hom}(a, y)$su punti generalizzati , dove un punto generalizzato di$x$ è solo un qualsiasi morfismo $a \to x$qualunque cosa. Questo ci permette di interpretare i morfismi$x \le y$in un ordine parziale come funzioni (necessariamente uniche) dai downsets $\{ a : a \le x \}$ ai downsets $\{ a : a \le y \}$, vale a dire la funzione unica di invio $a$ per $a$.

3. Inoltre, gli oggetti non iniziano con una particolare interpretazione in termini di tipi. La teoria dei tipi è un modo particolare di guardare alle categorie, o un modo particolare di generarle, e non è l'unico. Nella semantica categoriale standard per le teorie dei tipi, gli oggetti sono (interpretati come) tipi$A$ e morfismi $f : A \to B$ sono (interpretate come) funzioni con tipo di input $A$ e il tipo di output $B$. Se una categoria ha un oggetto terminale $1$ (che può essere interpretato come un tipo di unità) quindi morfismi $1 \to A$ può essere interpretato come termini di tipo $A$e un morfismo $f : A \to B$ quindi induce una funzione genuina $\text{Hom}(1, A) \to \text{Hom}(1, B)$ invio di termini di tipo $A$ a termini di tipo $B$. Spesso non ci sono abbastanza "punti" (functions$1 \to A$) per rendere questa operazione interessante in molte categorie, però; per esempio, in posets$1$, se esiste, è un elemento massimale , quindi$\text{Hom}(1, A)$ è vuoto a meno che $A$ è anche massimale.