Lemme de Yoneda: Le exemple

Introduction à la théorie des Catégories

Pour reprendre sur la seconde remarque de mon commentaire sur le lemme de Yoneda, l’exemple qui m’a fait comprendre Yoneda (disons, atteindre la compréhension niveau 1 de Yoneda, parce que ce truc est diantrement profond), c’est la catégorie des contextes du lambda-calcul simplement typé. C’est la catégorie dont je parle au début de ce message.
Pour résumer, ses objets sont les contextes de typage genre $latex Gamma = (x_1: tau_1 ldots x_n: tau_n)$ et ses morphismes de $latex Gamma$ vers $latex Delta = (y_1: tau’_1 ldots y_m: tau’_m)$ sont les séquences $latex f = (e_1 ldots e_m)$, avec $latex Gamma vdash e_i : tau’_i$. On peut voir un tel morphisme comme une substitution $latex text{[} y_1 mapsto e_1 ldots y_m mapsto e_m text{]}$ et c’est comme ça qu’on définit la composition: cette substitution envoie n’importe quel terme typé dans $latex Delta$ vers un terme du même type dans $latex…

View original post 225 mots de plus

Laisser un commentaire

Entrez vos coordonnées ci-dessous ou cliquez sur une icône pour vous connecter:

Logo WordPress.com

Vous commentez à l'aide de votre compte WordPress.com. Déconnexion / Changer )

Image Twitter

Vous commentez à l'aide de votre compte Twitter. Déconnexion / Changer )

Photo Facebook

Vous commentez à l'aide de votre compte Facebook. Déconnexion / Changer )

Photo Google+

Vous commentez à l'aide de votre compte Google+. Déconnexion / Changer )

Connexion à %s