Types ou catégories

Désolé pour la neutralisation, je n'aurais pas dû lancer le débat :-(

Merci Ignatus d’avoir rouvert un fil ici !! :-)

Je répondrai oui aux deux questions :
- Sans pouvoir trop argumenter mon point de vue, je verrais plutôt ces deux points de vue comme parallèles. Cependant, autant il est clair pour moi que les types ont une portée en tant que fondations ; autant, j’ai plutôt tendance à voir les catégories comme un point de vue sur les maths.
- Oui, il est possible de définir les catégories dans le cadre de la théorie des types

Première remarque:
Déjà, on peut définir les ensembles en théorie des types ; et donc, à partir de là, les catégories (sans s'embêter des problèmes : ensembles/collections, etc. ; si tu veux on peut définir les U-petites-catégories).
Mais bon, ça revient un peu à botter en touche.

Deuxième remarque:
Avant de se poser la question : comment définir les catégories en théorie des types, il vaut mieux déjà savoir comment définir les groupes en théorie des types !

Sinon, une première ébauche de définition partirait de la façon suivante :

Une catégorie est :
• un type C tel que
• pour tous x,y: C je me donne un type C(x,y),
• et un élément id_x : C(x,x)
• tels que pour tous x,y,z:C, je me donne une fonction C(x,y) x C(y,z) -> C(x,z)
• et je me donne un élément de Id(A,B) où A est C(x,y) -> C(x,y) x C(y,y) -> C(x,y) et où B = la fonction identité de C(x,y)->C(x,y)
(ie, en termes ensembliste, je demande que C(x,y) -> C(x,y) x C(y,y) -> C(x,y) = identité)
• et de même telles que C(x,y) -> C(x,x) x C(x,y) -> C(x,y) soit la fonction identité
(ie, je me donne un élément de Id(C,D) où C=... et D=...)
• et je me donne pour tous x,y,z,t un élément de Id(E,F) où E = ( C(x,y)xC(y,z) ) x C(z,t) -> C(x,z) x C(z,t) -> C(x,t) )
et où F = C(x,y) x (C(y,z) x C(z,t) -> C(x,y) x C(y,t) -> C(x,t) )

Si on écrit exactement la définition de ce type, cela donne une très longue expression...

Est-ce clair ?

708 : ta construction est naturelle, mais il me semble (je me trompe sûrement) que si on fait "naïvement" comme ça, on tombe sur des embuches à la longue.

@Ignatus
De mon point de vue, a priori, un type n’a rien à voir avec les ordinateurs. On peut définir les types sans savoir ce qu’est un ordinateur, etc.

Pour mieux comprendre les types, je te conseille ce document : https://hott.github.io/book/nightly/hott-online-1212-g0d25f68.pdf Pas tout évidemment : uniquement le chapitre 1 et l’appendice. Ça peut paraître audacieux, mais c’est je pense l’une des meilleures introductions.

La vidéo est sympathique aussi. À voir, un peu comme un divertissement.

Pour la question de définir un ensemble en théorie des types, elle me semble un peu prématurée vu tes connaissances en théorie de types. C’est fait dans le document mis en lien plus haut.

@Max
Je n’en sais rien ! J’ai juste fait la chose naturelle !
Je veux bien croire que ça ne marche pas en bout de course. Si tu as des références là-dessus, ça m’intéresse.