2. FONDEMENTS CATÉGORIQUES
Le chapitre précédent a posé sans les construire les objets sur lesquels reposent les quatre postulats. Rien de ce qui suit n'est propre à K7PL : chaque construction appartient au corpus stabilisé de la sémantique catégorique de la logique linéaire, et l'apport de ce chapitre est d'y identifier exactement les briques dont les postulats ont besoin — ni plus, ni moins — puis de les assembler dans l'ordre où elles s'appellent. Ce parti de conservation se paie en asymétries de preuve, signalées au fil du texte.
Une remarque d'orientation, qui commande la lecture du chapitre entier. On y construit un système de types de la manière intrinsèque — les types sont des objets de C, les termes des morphismes — alors que l'architecture du langage est extrinsèque de bout en bout. Un jugement à trois composantes porté au-dessus d'un terme, dont la Phase 8 retire tout ce qui appartient à la compilation. Cet écart n'est pas une gêne à surmonter, c'est la définition même d'un système de raffinement de types — un foncteur de la catégorie des dérivations vers celle des termes sous-jacents [1] — et ce chapitre construit le domaine de ce foncteur.
Chacune des quatre sections qui suivent y contribue par une pièce, et la cinquième les rassemble. La catégorie ambiante donne les objets et les flèches au-dessus desquels les dérivations se portent. La comonade exponentielle et ses fragments donnent les morphismes verticaux, ceux qui ne changent rien au terme sous-jacent et tout à ce qu'il exige. Les algèbres et coalgèbres donnent les schémas de définition que ce foncteur devra préserver. L'enrichissement donne l'ordre dans lequel deux dérivations de même image se comparent. Le §2.5 montre alors que ces quatre pièces sont celles d'un système de raffinement, et ce que cette lecture dispense de poser séparément.