ET2CSC.md

Cadre logique et contexte : La théorie ET2CSC (Elementary Theory of the 2-Category of Small Categories) est une théorie du premier ordre qui axiomatise la structure de 2-catégorie des petites catégories, foncteurs et transformations naturelles, sans supposer de théorie des ensembles sous-jacente. On considère une 2-catégorie $K$ comme structure de premier ordre avec ses objets (0-cellules), ses morphismes (1-cellules) et ses 2-morphismes (2-cellules), munie des opérations de composition horizontale et verticale et des identités, satisfaisant les conditions de cohérence usuelles (unités et associativité strictes). Un modèle typique de ET2CSC est de la forme $K = \Cat(E)$, où $E$ est une catégorie satisfaisant les axiomes de la théorie élémentaire de la catégorie des ensembles (ETCS de Lawvere). Dans ce cas, $K = \Cat(E)$ désigne la 2-catégorie dont les objets sont les petites catégories internes à $E$, les 1-cellules sont les foncteurs internes, et les 2-cellules sont les transformations naturelles internes. Cette 2-catégorie $\Cat(E)$ est dite la 2-catégorie des petites catégories dans $E$. Les axiomes de ET2CSC permettront précisément de caractériser les 2-catégories isomorphes à une telle $\Cat(E)$ lorsque $E$ est un modèle de ETCS.

Catégories internes : Une catégorie interne dans $E$ est définie par un diagramme simplicial tronqué $A: \Delta_{\le 3}^{op} \to E$ satisfaisant les conditions de Segal (envoyant certains carrés de $\Delta_{\le 3}$ sur des carrés cocartésiens dans $E$). Concrètement, il s’agit de la donnée $(A_0, A_1, d_0, d_1, i, m)$ où $A_0$ est l’objet des objets, $A_1$ l’objet des arrows (flèches) dans $E$, avec $d_0, d_1: A_1 \to A_0$ (source et but), $i: A_0 \to A_1$ (insertion des identités) et $m: A_1 \times_{d_0, A_0, d_1} A_1 \to A_1$ (loi de composition). Ces données satisfont les axiomes habituels d’une catégorie (identités comme unités pour $m$, et associativité de $m$). On note généralement $A = (A_0, A_1)$ pour une catégorie interne.

Foncteurs internes : Étant donnés deux catégories internes $A = (A_0, A_1)$ et $B = (B_0, B_1)$ dans $E$, un foncteur interne $f: A \to B$ est donné par un couple $(f_0: A_0 \to B_0,; f_1: A_1 \to B_1)$ de morphismes de $E$ préservant la structure de catégorie (c’est un morphisme de diagrammes $\Delta_{\le3}^{op} \to E$ entre $A$ et $B$). Intuitivement, $f_0$ envoie chaque objet de $A$ sur un objet de $B$, et $f_1$ envoie chaque flèche de $A$ sur une flèche de $B$, de sorte que $d_0^B \circ f_1 = f_0 \circ d_0^A$ et $d_1^B \circ f_1 = f_0 \circ d_1^A$, et respectant $i$ et $m$ (l’identique et la composition).

Transformations naturelles internes : Si $f,g: A \to B$ sont deux foncteurs internes (i.e. $f=(f_0,f_1)$ et $g=(g_0,g_1)$), une transformation naturelle interne $\alpha: f \Rightarrow g$ est définie par un morphisme (appelé assignateur de composantes) $\alpha: A_0 \to B_1$ dans $E$ qui assigne à chaque objet $x \in A_0$ une flèche $\alpha(x): f_0(x) \to g_0(x)$ de $B$, de manière naturelle. Plus précisément, $\alpha$ doit satisfaire les conditions de commutativité internes suivantes : (1) pour chaque objet $x$ de $A_0$, $d_0^B(\alpha(x)) = f_0(x)$ et $d_1^B(\alpha(x)) = g_0(x)$ (condition d’assignation de composantes), et (2) pour chaque flèche $u: x \to y$ de $A_1$, on a $g_1(u) \circ \alpha(x) = \alpha(y) \circ f_1(u)$ dans $B_1$ (condition de naturalité interne). Graphiquement, $\alpha$ fournit pour chaque $u: x \to y$ dans $A$ un 2-carré commutatif dans $E$ reliant $f(u)$ et $g(u)$.

2-catégorie $\Cat(E)$ : Les catégories internes dans $E$, les foncteurs internes et les transformations naturelles internes forment une 2-catégorie, notée $\Cat(E)$. La catégorie sous-jacente $\Cat(E)_1$ (où l’on oublie les 2-cellules) a pour objets les catégories internes et pour flèches les foncteurs internes. Les 2-cellules (transformations naturelles internes) permettent de composer verticalement (composition ordinaire de transformations) et horizontalement (par whiskering, i.e. composition avec pré- ou post-composition de foncteurs) comme dans toute 2-catégorie. Ainsi $\Cat(E)$ est bien une 2-catégorie stricte. Si $E$ est localement petite, alors $\Cat(E)$ est une 2-catégorie localement petite (chaque hom-catégorie $\Cat(E)(A,B)$ est essentiellement petite).

Notations et conventions : Dans $\Cat(E)$, on distingue souvent un objet $X$ de $K=\Cat(E)$ comme étant discret si toute 2-cellule entrant dans $X$ est nécessairement une identité (intuitivement, $X$ n'a pas de structure de 2-cellules non triviales). On note $\Disc(K)$ la sous-catégorie pleine de $K$ formée de ses objets discrets. D’autre part, on définit deux foncteurs importants entre $E$ et $\Cat(E)$:

• Le foncteur disc: $E \to \Cat(E)_1$ (où $\Cat(E)_1$ désigne la catégorie sous-jacente) envoie chaque objet $X \in E$ sur une catégorie interne $\disc(X)$ appelée catégorie discrète sur $X$, définie comme la catégorie interne constante égale à $X$ (mêmes objets et flèches égales aux identités). Ainsi, $\disc(X)$ a $X$ pour ensemble d’objets et uniquement des identités comme flèches. Ce foncteur $\disc: E \to \Cat(E)$ est pleinement fidèle (il réalise $E$ comme les objets discrets de $\Cat(E)$).
• Le foncteur $(\minus)_0: \Cat(E)_1 \to E$ envoie chaque catégorie interne $A$ sur son objet des objets $A_0 \in E$ (on le note parfois $\Pi_0(A)$ car il correspond aux composantes connexes dans certains cas, voir ci-dessous). C’est un foncteur 2-fonctoriel évident (oubli des flèches).

Sous des conditions modérées, ces foncteurs forment des adjoints :

• Adjoint à gauche de $(\minus)_0$: Le foncteur $\disc: E \to \Cat(E)_1$ est adjoint à gauche de $(\minus)_0$ (on a $\disc \dashv (\minus)_0$). L’unité de l’adjonction est l’identité, et la counité $\epsilon_A: \disc((A)_0) \to A$ en un objet $A$ est donnée par le foncteur interne qui inclut les objets de $A$ comme objets discrets et utilise $i: A_0 \to A_1$ pour les flèches. Cette counité est universelle pour les foncteurs réfléchissant les identités (i.e. si $f: A \to B$ est un foncteur interne qui envoie toute flèche identité de $A$ sur une identité de $B$, alors $f$ se factorise de façon unique par $\epsilon_A$). Notez que $\disc$ préserve les limites finies.
• Adjoint à droite de $(\minus)_0$: Si $E$ possède des produits finis, alors $(\minus)_0: \Cat(E)_1 \to E$ admet un adjoint à droite noté $\indisc: E \to \Cat(E)_1$ (parfois appelé codiscrétisation). Pour $X \in E$, $\indisc(X)$ est la catégorie interne indiscrète sur $X$ : elle a pour ensemble d’objets $X$ et pour chaque paire d’objets une unique flèche (on remplit trivialement tous les hom-sets). Le foncteur $\indisc$ est pleinement fidèle et son adjonction avec $(\minus)_0$ a pour unité $\eta_A: A \to \indisc((A)_0)$ sur $A$, qui est le foncteur interne identique sur les objets et donné par $(d_0, d_1): A_1 \to A_0 \times A_0$ sur les flèches. Intuitivement, $\eta_A$ “oublie” toute structure non triviale de $A$ en la factorisant à travers la catégorie chaotique sur $A_0$. Une conséquence utile : $f: A \to B$ est un foncteur interne pleinement fidèle si et seulement si le carré de naturalité $\eta_B \circ f = \indisc(f_0) \circ \eta_A$ est un carré cartésien dans $E$.
• Autre adjoint (foncteur $\Pi_0$): Si $E$ possède en outre les coégalisateurs des paires réflexives, alors le foncteur $\disc: E \to \Cat(E)_1$ admet à son tour un adjoint à gauche $\Pi_0: \Cat(E)_1 \to E$. Pour chaque catégorie interne $A$, $\Pi_0(A)$ est le coégalisateur dans $E$ de $d_0, d_1: A_1 \rightrightarrows A_0$ (intuitivement, l’“ensemble” des composantes connexes de $A$). En effet, $\Pi_0(A)$ s’identifie à l’objet des coins d’isomorphisme de $A$ (coequalizer des deux projections), ce qui généralise la construction de l’ensemble des composantes connexes d’une catégorie classique. Le foncteur $\Pi_0$ envoie un foncteur interne $f: A \to B$ sur le morphisme $\Pi_0(f): \Pi_0(A) \to \Pi_0(B)$ induit par l’universalité du coégalisateur. Ainsi on obtient la chaîne d’adjonctions $\Pi_0 \dashv \disc \dashv (\minus)_0 \dashv \indisc$ reliant $E$ et $\Cat(E)$.

Axiomes (ET2CSC)

Définition 9.1 (Modèle de ET2CSC). On dit qu’une 2-catégorie $K$ modélise la théorie élémentaire de la 2-catégorie des petites catégories (ET2CSC) si elle satisfait toutes les propriétés suivantes:

1. $K$ satisfait les cinq conditions de base de la Proposition 3.1 (qui font de $K$ une 2-catégorie du type $\Cat(E)$ avec $E$ ayant certains limites; voir ci-dessous).
2. $K$ admet un objet terminal (noté $1$).
3. $K$ est fermé cartésien (c’est-à-dire admet des hom internes/exponentiels — voir Théorème 4.1 pour la définition).
4. $K$ est 2-bien-pointée (2-well-pointed) au sens de la Définition 5.12 (voir plus loin).
5. $K$ possède un objet nombres naturels au sens de la Définition 6.1 (point (2)).
6. $K$ possède un classifieur de sous-objets pleins au sens de la Définition 7.1 (point (3)).
7. $K$ satisfait l’axiome de choix catégorifié au sens de la Définition 8.11.

Ces sept conditions sont les axiomes de la théorie ET2CSC. Intuitivement, elles correspondent aux axiomes de ETCS traduits dans $K = \Cat(E)$ : chacune assure que $E$ sous-jacente est une catégorie de ensembles bien connue. En particulier, si $E$ est une catégorie qui modélise ETCS (au sens de la Définition 1.1 ci-dessous), alors $K=\Cat(E)$ modélise ET2CSC. Réciproquement, si $K$ modélise ET2CSC, alors $E = \Disc(K)$ (la catégorie des objets discrets de $K$) modélise ETCS et $K \cong \Cat(E)$.

Définition 1.1 (Modèle de ETCS, d’après Lawvere [Law64]). Une catégorie $E$ est dite modèle de la théorie élémentaire de la catégorie des ensembles (ETCS) si les six conditions suivantes sont satisfaites: (1) $E$ a des limites finies (produit fibré et objet terminal, donc notamment $E$ a un objet terminal $1$). (2) $E$ est fermée cartésienne (i.e. possède des exponentielles $Y^X$ pour tous objets $X,Y$). (3) L’objet terminal $1$ est un générateur de $E$ (équivalemment, la famille ${1}$ est génératrice dans $E$ au sens de la Définition 5.8(1) – ceci caractérise ce qu’on dit aussi $E$ bien-pointée). (4) $E$ possède un objet des nombres naturels (NNO, natural numbers object). (5) $E$ possède un classifieur de sous-objets (un monomorphisme $\top: 1 \to \Omega$ classifiant les sous-objets de $E$). (6) $E$ satisfait l’axiome externe du choix, c’est-à-dire que tout épimorphisme dans $E$ admet une section (Définition 8.1).

Ces axiomes (1)–(6) sont exactement ceux de Lawvere pour axiomatiser la catégorie des ensembles usuels dans une théorie du premier ordre.

Définitions

Nous rassemblons ici les principales définitions formelles introduites dans l’article, pour servir de référentiel au raisonnement de l’assistant.

Définition 5.8 (Famille génératrice). (1) Une famille d’objets $G$ dans une catégorie $C$ est dite génératrice si la famille de foncteurs $C(X, -): C \to \Ens$ pour $X \in G$ est conjointement fidèle (c’est-à-dire que toute paire de flèches distinctes dans $C$ peut être distinguée par au moins un $X \in G$). (2) De même, une famille d’objets $\mathcal{G}$ dans une 2-catégorie $K$ est dite génératrice si, pour toute paire de 1-cellules $f \neq g: A \to B$, il existe un objet $X \in \mathcal{G}$ et une 2-cellule $\Disc(X) \to B$ (via une 1-cellule $\Disc(X) \to A$) qui distingue $f$ et $g$. Autrement dit, les foncteurs 2-fonctoriels $K(X, -): K \to \Cat$ pour $X \in \mathcal{G}$ sont conjointement fidèles. En particulier, dire que “$1$ est un générateur de $E$” signifie que la famille ${1}$ est génératrice, et dire que “$2 \odot 1$ est un générateur de $K$” signifie que la famille ${2 \odot 1}$ l’est (voir ci-après la définition de $2$-bien-pointé).

Définition 5.12 (2-bien-pointé). Une 2-catégorie $K$ est dite 2-bien-pointée (2-well-pointed) si les trois conditions suivantes sont vérifiées: (1) $K$ possède un objet terminal $1$. (2) Le copuissance $2 \odot 1$ existe dans $K$ (où $2$ désigne la petite catégorie flèche libre à deux objets et une flèche non triviale). (3) La famille ${,2 \odot 1,}$ est génératrice de $K$ (au sens de la Définition 5.8(2)).

Remarque: Dans $K=\Cat(E)$, la copuissance $2 \odot 1$ s’interprète concrètement comme la catégorie interne $2_E$ construite dans $E$ qui représente l’ajout d’une flèche générique (voir Définition 5.4). Ainsi $2 \odot 1 = 2_E$. La condition (3) revient alors à dire que $2_E$ est générateur dans $\Cat(E)$, ce qui équivaut (par le Lemme 5.2 et le Corollaire 5.9 ci-dessous) à ce que $E$ soit bien-pointée.

Définition 6.1 (Objet des nombres naturels). (1) Un objet des nombres naturels (NNO) dans une catégorie $C$ avec objet terminal $1$ est la donnée de deux flèches $1 \xrightarrow{z} N \xleftarrow{s} N$ (respectivement zéro et successeur) telle que pour tout objet $X$ et flèches $1 \xrightarrow{f} X \xleftarrow{g} X$, il existe une unique flèche $u: N \to X$ vérifiant $u \circ z = f$ et $u \circ s = g \circ u$. Cela exprime que $N$ avec $z, s$ est un objet initial dans la catégorie des diagrammes en $X$ de la forme $1 \to X \leftarrow X$. C’est une reformulation de l’énoncé: $N$ est l’algèbre initiale de l’endofoncteur $X \mapsto 1 + X$. (2) De même, un objet des nombres naturels dans une 2-catégorie $K$ (avec $1$ terminal) est la donnée de 1-cellules $1 \xrightarrow{z} N$ et $N \xrightarrow{s} N$ telles que, pour toute 1-cellule $1 \xrightarrow{f} X$ et $X \xrightarrow{g} X$ dans $K$, il existe une 1-cellule $u: N \to X$ et une 2-cellule isomorphe $u \circ s \Rightarrow g \circ u$ (qu’on peut voir comme la “même” condition $u s = g u$ mais en tenant compte de la 2-catégorie) qui sont essentiellement uniques, satisfaisant $u \circ z = f$. Autrement dit, $(N, z, s)$ réalise un objet initial dans la 2-catégorie des anamorphismes de $X$ dans $K$ (voir Remarque 8.13 ci-dessous). Dans $K = \Cat(E)$, on montre que si $E$ a un objet des nombres naturels $N$, alors $\indisc(N)$ est un objet des nombres naturels dans $\Cat(E)$, et réciproquement. En particulier, $N$ est discret dans $\Cat(E)$ (ses 2-cellules sont seulement les identités).

Définition 7.1 (Classifieur de sous-objets pleins). (1) Rappelons qu’un monomorphisme dans $\Cat(E)$ (ou dans toute 2-catégorie) est un foncteur interne $i: X \to Y$ dont la composante sur les objets $i_0: X_0 \to Y_0$ est un monomorphisme dans $E$ et qui, de plus, est fidèle (injectif sur les 2-cellules incidentes). Si en outre $i$ est pleinement fidèle (au sens de la Définition 2.11, c’est-à-dire qu’il induit des bijections sur chaque hom interne), on l’appelle un monomorphisme pleinement fidèle ou inclusion de sous-objet plein. (2) Un sous-objet plein de $Y$ est la donnée d’un monomorphisme pleinement fidèle $i: X \hookrightarrow Y$. On dit aussi que $X$ est un sous-objet plein de $Y$. (3) Un classifieur de sous-objets pleins dans une 2-catégorie $K$ est un monomorphisme pleinement fidèle $\top: 1 \to \Omega$ dans $K$ tel que pour tout monomorphisme pleinement fidèle $i: X \hookrightarrow Y$, il existe une unique 1-cellule $\chi_i: Y \to \Omega$ rendant le carré suivant cartésien (un pullback strict):

X ──> Y
│      │ χ_i
│      │ 
1 ──> Ω

Autrement dit, $X$ est (isomorphe à) le pullback de $\top: 1 \to \Omega$ le long de $\chi_i: Y \to \Omega$. La 1-cellule $\chi_i: Y \to \Omega$ est appelée la flèche classifiante du sous-objet plein $i$. Lorsque $K = \Cat(E)$, un classifieur de sous-objets pleins $\top: 1 \to \Omega$ équivaut à un certain objet $\Omega_0 = (\Omega)_0$ dans $E$ qui joue le rôle d’“ensemble des sous-objets pleins” (voir Proposition 7.5 ci-dessous), et on montre que $\indisc(\top): \indisc(1) \to \indisc(\Omega_0)$ est un tel classifieur dans $\Cat(E)$ dès que $E$ a un classifieur de sous-objets. En fait, lorsque $E$ est un topos élémentaire, $\disc(\top_E): 1 \to \disc(\Omega_E)$ (avec $\top_E: 1 \to \Omega_E$ le classifieur de sous-objets ordinaire de $E$) devient un classifieur de sous-objets pleins dans $\Cat(E)$.

Définition 8.1 (Axiome externe du choix). On dit qu’une catégorie $E$ satisfait l’axiome externe du choix si tout épimorphisme $e: X \twoheadrightarrow Y$ dans $E$ admet une section $s: Y \to X$ (c’est-à-dire $e \circ s = \mathrm{id}_Y$). Cette condition est l’analogue catégorique de l’axiome du choix classique (toute surjection possède une section).

Définition 8.10 (Flèche aiguë). Dans une 2-catégorie $K$, on appelle flèche aiguë (acute morphism) toute 1-cellule $f: X \to Y$ qui est à la fois pleinement fidèle et left orthogonal à toute inclusion de sous-objet plein. Plus explicitement, $f$ est aiguë si pour tout carré commutatif $p: A \to X$, $q: B \to Y$ avec $q$ monomorphisme pleinement fidèle, il existe une unique 1-cellule $u: B \to X$ telle que $f \circ u = q$ et $p = u \circ s$ (où $s: A \to B$ est l’inclusion). Intuitivement, une flèche pleinement fidèle est aiguë si elle est “sur les objets” de façon suffisamment forte (cf. Remarque 8.13 : si $E$ est régulière, cela équivaut à dire que $f_0: X_0 \to Y_0$ est un épimorphisme régulier dans $E$). On désigne souvent par $(L, R) = (\text{flèches aiguës}, \text{monos pleins})$ le système de factorisation orthogonale correspondant (voir Prop 8.7).

Définition 8.11 (Axiome de choix catégorifié). On dit qu’une 2-catégorie $K$ satisfait l’axiome de choix catégorifié si toute 1-cellule $f: X \to Y$ qui est à la fois pleinement fidèle et aiguë admet une section (c’est-à-dire qu’il existe une 1-cellule $s: Y \to X$ avec $f \circ s = \id_Y$). Cette condition est l’analogue en dimension 2 de l’axiome du choix, où l’hypothèse “épimorphisme” est remplacée par “foncteur pleinement fidèle aigu” (notion de « surjection sur les objets » dans $\Cat(E)$).

Définition 9.4 (Morphismes de modèles). (1) Si $E$ et $E'$ sont des catégories modélisant ETCS, un ETCS-morphisme $F: E \to E'$ est un foncteur qui préserve les limites finies, les hom internes (exponentiels), le classifieur de sous-objets, et l’objet des nombres naturels. En d’autres termes, $F$ est un foncteur qui envoie la structure ETCS de $E$ vers celle de $E'$ (on dit aussi que $F$ est un foncteur lex cartésien fermé et qui préserve NNO et subobject classifier). (2) Si $K$ et $K'$ modélisent ET2CSC, un ET2CSC-morphisme $F: K \to K'$ est un 2-foncteur (foncteur 2-catégorique strict) qui préserve les pullbacks, les copuissances par $2$, les objets codescent de cateades (voir Prop 3.1) ainsi que l’objet terminal, les hom internes, le classifieur de sous-objets pleins et l’objet des nombres naturels. Intuitivement, $F$ préserve toutes les structures énumérées dans la Définition 9.1. (On peut voir qu’il préserve alors automatiquement les autres propriétés comme l’axiome du choix catégorifié, car celles-ci découlent logiquement des précédentes.)

Théorèmes et Propositions

Cette section énumère les principaux résultats démontrés dans l’article, en correspondance avec les axiomes ci-dessus. Ils établissent l’équivalence entre les propriétés de $E$ (ETCS) et de $K=\Cat(E)$ (ET2CSC), ainsi que la caractérisation catégorique des modèles de ET2CSC et leurs morphismes.

Proposition 3.1 (d’après Théorème 4.18 de [Bou10]). Soit $E$ une catégorie avec pullbacks (produits fibrés). Alors la 2-catégorie $K := \Cat(E)$ satisfait les conditions suivantes :

1. $K$ admet des pullbacks (2-limites finies strictes) et des puissances par $2$ (c’est-à-dire des coproduits “exponentiels” $2 \pitchfork (-)$).
2. $K$ possède des objets codescent pour toute catégorie interne dans $K$ dont les applications source et but forment une fibrations discrètes de part et d’autre (ces objets codescent, appelés cateades dans $K$, sont les colimites 2-catégoriques analogues des objets coégalisateurs simpliciaux tronqués).
3. Les morphismes de codescent sont effectifs dans $K$ (toute coequalisation de cateades est un quotient effectif au sens 2-catégorique).
4. Les objets discrets de $K$ sont projectifs (au sens de [Bou10, Def. 4.13]) – c’est une propriété analogue à l’existence d’ensembles projectifs générateurs.
5. Pour chaque objet $A ∈ K$, il existe un objet projectif $P ∈ K$ et un morphisme de codescent $c: P \to A$.

Réciproquement, si une 2-catégorie $K$ satisfait (1)–(5) ci-dessus, alors $K$ est 2-équivalente à $\Cat(E)$ pour une certaine catégorie $E$ avec pullbacks (plus précisément $E := \Disc(K)$).

Remarque 3.2. On travaillera généralement avec les 2-catégories $K$ satisfaisant ces conditions de base (1)–(5). Cette proposition due à J. Bourke nous permet d’utiliser librement la théorie des catégories internes dans nos preuves, même pour établir des propriétés formulées à première vue en termes purement 2-catégoriques. (Le lecteur peut admettre Prop 3.1 comme une “boîte noire”, mais nous en donnons l’intuition : la condition de puissance par $2$ assure l’existence de certaines structures carrées; les cateades capturent la notion de colimites simpliciales tronquées, généralisant les coégalisateurs; etc.)

Proposition 3.3. La 2-catégorie $\Cat(E)$ possède toutes les 2-limites finies si et seulement si la catégorie $E$ possède toutes les limites finies. En particulier, $\Cat(E)$ a un objet terminal si et seulement si $E$ en a un (ce qu’on utilise dans l’axiome (2) de ET2CSC).

Théorème 4.1. Soit $E$ une catégorie avec limites finies. Alors $E$ est fermée cartésienne (admet des exponentielles) si et seulement si la 2-catégorie $\Cat(E)$ est fermée cartésienne (c’est-à-dire admet des hom internes). Dans ce cas, le foncteur $\disc: E \to \Cat(E)$ préserve les hom internes (en particulier $\disc$ transforme l’exponentielle $Y^X$ en l’hom interne $\Cat(E)(\disc(X), \disc(Y))$).

Esquisse de preuve. Si $E$ est fermée cartésienne, on peut construire explicitement des hom internes dans $\Cat(E)$: étant donné deux catégories internes $A, C$, leur hom interne $[A, C]$ est la catégorie interne des foncteurs de $A$ vers $C$ et transformations internes (définie via un foncteur nerve $N: \Cat(E) \to [\Delta^{op}, E]$ qui identifie $\Cat(E)$ à un idéal exponentiel de $[\Delta^{op}, E]$). Réciproquement, si $\Cat(E)$ est fermé cartésien, en particulier il possède l’hom interne $[\disc(X), \disc(Z)]$ pour tous objets $X, Z$ de $E$. Or on montre que $[\disc(X), \disc(Z)]$ a pour ensemble d’objets $Z^X$ dans $E$ (grâce à $\disc \dashv (\minus)_0$), ce qui exhibe directement l’exponentielle $Z^X$ dans $E$. Ainsi $E$ est fermé cartésien. (Voir [BE72] pour un argument alternatif via le théorème de réflexion de Day.)

Définition 5.1. (1) On dit qu’une catégorie avec pullbacks $E$ est extensive si elle admet des coproducts finis et que pour tous objets $A, B$ de $E$, le foncteur canonique $E/(A+B) \to E/A \times E/B$ (du produit fibré des catégories des objets au-dessus de $A$ et $B$ vers la catégorie au-dessus de $A+B$) est une équivalence de catégories. Si de plus $E$ admet un objet terminal, on dit que $E$ est lextensive (extensive avec un 1). (2) De même, on dit qu’une 2-catégorie $K$ (avec pullbacks) est extensive si elle admet des coproduits finis (2-catégoriques) et que le 2-foncteur $K/(A \sqcup B) \to K/A \times K/B$ est une 2-équivalence pour tous $A, B$. Si en outre $K$ a un objet terminal $1$ et admet les puissances $2 \pitchfork (-)$, on dit que $K$ est lextensive.

Lemme 5.2. Soit $E$ une catégorie avec pullbacks et produits. Alors $E$ est extensive si et seulement si $\Cat(E)$ est extensive (i.e. $E$ extensive implique $\Cat(E)$ extensive, et inversement). En particulier, si $E$ est lextensive, $\Cat(E)$ l’est aussi, et vice versa.

Remarque 5.3. Dans une catégorie extensive, les sommes disjointes bénéficient d’un foncteur de somme indépendante qui commute aux produits fibrés (voir [CLW93]). Dans une 2-catégorie extensive $K$, on a de plus que $K$ est lextensive ssi elle a un objet terminal et des puissances $2 \pitchfork (-)$. Dans $\Cat(E)$, on peut construire explicitement la copuissance $2_E = 2 \odot 1$ comme la catégorie interne libre sur une flèche dans $E$ (voir Définition 5.4). Ce $2_E$ joue le rôle de “$2$ à puissancer”.

Définition 5.4. (Construction de $2_E$) Soit $S = \Fin$-$\Ens$ la catégorie des ensembles finis et fonctions. On applique alors le 2-foncteur $\Cat(F): \Cat(\Fin\text{-}\Ens) \to \Cat(E)$, où $F: \Fin\text{-}\Ens \to E$ est le foncteur qui envoie l’ensemble final $1$ de $\Fin\text{-}\Ens$ sur $1 \in E$ et préserve coproducts finis. Ce $F$ existe et est unique par propriétés universelles. L’image par $\Cat(F)$ de la catégorie flèche libre $2 = {0 \to 1}$ (objet final librement muni d’une flèche non triviale) est une catégorie interne dans $E$, notée $2_E$. Par construction, $2_E$ est un objet discret sur deux objets avec une flèche entre eux dans $\Cat(E)$. On montre que $2_E$ est précisément la copuissance $2 \odot 1$ dans $\Cat(E)$.

Théorème 5.5. Si $E$ est lextensive et fermée cartésienne, alors $2_E$ (défini ci-dessus) existe et la 2-catégorie $\Cat(E)$ admet les copuissances par $2$. Plus précisément, pour tout objet $X$ de $\Cat(E)$, $2 \odot X$ existe et vaut $2_E \times X$ (produit dans $\Cat(E)$). En particulier, $\disc: E \to \Cat(E)$ préserve les coproduits et les copuissances par 2.

Corollaire 5.9. Soit $E$ une catégorie possédant des limites finies, des coproducts extensifs, et une famille génératrice d’objets $G$. Alors la famille $G^b := {,2_E \times \disc(X) \mid X \in G,}$ est une famille génératrice d’objets de $\Cat(E)$. Autrement dit, on peut obtenir une famille génératrice de $\Cat(E)$ en prenant la copuissance $2_E$ du générateur de $E$. En particulier, si $E$ est bien-pointée ($G={1}$), on obtient que ${2_E}$ est génératrice de $\Cat(E)$, c’est-à-dire $\Cat(E)$ est 2-bien-pointée. Réciproquement, si $\Cat(E)$ est 2-bien-pointée, alors $E$ est bien-pointée (c’est essentiellement le même argument en sens inverse, en utilisant $\Pi_0$).

Théorème 5.14. Soit $E$ une catégorie lextensive et fermée cartésienne. Alors $E$ est bien-pointée (i.e. $1$ est un générateur de $E$) si et seulement si $\Cat(E)$ est 2-bien-pointée (au sens de Définition 5.12).

Preuve (idée). ($\Rightarrow$) Si $E$ est bien-pointée, par Cor. 5.9 avec $G={1}$ on a que $\Cat(E)$ a ${2_E}$ générateur. De plus $1$ terminal dans $E$ donne $1$ terminal dans $\Cat(E)$, et $2_E = 2 \odot 1$ existe par Th. 5.5. Donc $\Cat(E)$ est 2-bien-pointée. ($\Leftarrow$) Réciproquement, si $\Cat(E)$ est 2-bien-pointée, en particulier $2_E$ existe et ${2_E}$ est générateur. Par adjonction $\Pi_0 \dashv \disc$, l’objet $\Pi_0(2_E)$ est un coégalisateur de $d_0,d_1: (2_E)_1 \to (2_E)_0$ dans $E$. Mais $2_E$ étant obtenu par $2 \odot 1$, on voit que $(2_E)_0 = 1 + 1$ et $(2_E)_1 = 1$ (une unique flèche entre deux objets distincts); ainsi $\Pi_0(2_E) \cong 1$ (puisque $E$ a $1$ terminal). L’universalité de $\Pi_0(2_E)$ implique alors que $1$ est un objet générateur de $E$. Donc $E$ est bien-pointée.

Théorème 6.4. Soit $E$ une catégorie avec limites finies. Alors $E$ possède un objet des nombres naturels si et seulement si la 2-catégorie $\Cat(E)$ possède un objet des nombres naturels (au sens de Définition 6.1). Dans ce cas, l’objet des nombres naturels de $\Cat(E)$ est $\indisc(N)$ où $N$ est celui de $E$.

Remarque : Ainsi, les NNO sont en correspondance directe entre $E$ et $\Cat(E)$. Par exemple, si $E$ a un NNO $\mathbb{N}$, alors $\Cat(E)$ a pour NNO la catégorie indiscrète sur $\mathbb{N}$ (qui est une catégorie avec les entiers comme objets et une unique flèche entre chaque paire d’entiers). Cela implique aussi que les arithmétiques internes se correspondent dans $E$ et $\Cat(E)$.

Proposition 7.3. Supposons que $E$ possède un classifieur de sous-objets (ordinaire) $\top_E: 1 \to \Omega_E$. Alors $\indisc(\top_E): \indisc(1) \to \indisc(\Omega_E)$ est un classifieur de sous-objets pleins dans $\Cat(E)$.

Preuve (idée). $\indisc(\top_E)$ est un monomorphisme pleinement fidèle dans $\Cat(E)$. Prenons une inclusion de sous-objet plein $f: X \hookrightarrow Y$ dans $\Cat(E)$, ce qui signifie que $f_0: X_0 \to Y_0$ est mono dans $E$. Comme $\top_E$ classifie les monos de $E$, on a une flèche $\chi_{f_0}: Y_0 \to \Omega_E$ avec $X_0 = Y_0 \times_{\chi_{f_0},\Omega_E,\top_E} 1$. Alors $\chi_{f} := \indisc(\chi_{f_0}): Y \to \indisc(\Omega_E)$ est une flèche classifiante faisant de $X = \indisc(X_0)$ le pullback de $\indisc(\top_E)$ le long de $\chi_f$. L’unicité provient de l’unicité de $\chi_{f_0}$.

Proposition 7.5. Soit $E$ une catégorie avec objet terminal et pullbacks. Si $\Cat(E)$ admet un classifieur de sous-objets pleins $\top: 1 \to \Omega$, alors $\top_0: 1 \to \Omega_0$ est un classifieur de sous-objets dans $E$ (où $\Omega_0 := (\Omega)_0$).

Preuve (idée). Prenons un mono $i: A \hookrightarrow B$ dans $E$. Alors $\indisc(i): \indisc(A) \to \indisc(B)$ est un mono plein dans $\Cat(E)$. Par hypothèse de classifieur, il existe $\chi: B \to \Omega$ tel que $\indisc(A)$ soit le pullback de $\top$ le long de $\chi$. En particulier sur les objets: $A = A_0 = B_0 \times_{\chi_0, \Omega_0, \top_0} 1$, où $\chi_0: B_0 \to \Omega_0$ est la composante objet de $\chi$. Donc $\top_0: 1 \to \Omega_0$ classifie bien le mono $A_0 \hookrightarrow B_0$ dans $E$. (L’unicité est similaire.)

Théorème 7.7. Soit $E$ une catégorie lextensive, fermée cartésienne, avec limites finies. Alors $E$ possède un classifieur de sous-objets (ordinaire) si et seulement si $\Cat(E)$ possède un classifieur de sous-objets pleins. En particulier, pour $E$ topos élémentaire, $\Cat(E)$ a un classifieur de sous-objets pleins, et inversement si $\Cat(E)$ a un classifieur de sous-objets pleins on peut montrer que $E$ doit être extensive (Prop 7.10 ci-dessous) et donc un topos (puisque les autres propriétés ETCS assurent déjà que $E$ est un topos élémentaire).

Proposition 7.10. Si $\Cat(E)$ possède un classifieur de sous-objets pleins, alors : (1) $E$ est extensive; (2) $\Cat(E)$ est extensive. (On en déduit $E$ topos élémentaire en combinant (1) avec les propriétés (2),(4),(6) de ETCS.)

Théorème 8.12. Soit $E$ une catégorie avec pullbacks, produits finis et un système de factorisation orthogonale (L, R) donné par les épimorphismes et monomorphismes ($L = \text{Épi}$, $R = \text{Mono}$). Alors les deux assertions suivantes sont équivalentes: (1) $E$ satisfait l’axiome externe du choix. (2) La 2-catégorie $\Cat(E)$ satisfait l’axiome de choix catégorifié.

Preuve (idée). Dans $E$, l’axiome du choix dit que toute flèche $e$ dans $L$ admet une section. On veut montrer que cela équivaut à : toute flèche $f$ dans $L'$ (les “aiguës”) admet une section dans $\Cat(E)$. L’implication (1)$\Rightarrow$(2) résulte de la Proposition 8.4 ci-dessous en remarquant par Corollaire 8.8 que “$f_0$ épi” $\Leftrightarrow$ “$f$ est aiguë” dans $\Cat(E)$. Réciproquement, si toute $f$ aiguë a une section dans $\Cat(E)$, en particulier $\eta_A: A \to \indisc(A_0)$ admet une section pour chaque $A$ (car $\eta_A$ est aiguë et fully faithful). En composant avec la counité $\epsilon_A: \disc(A_0) \to A$, on obtient que tout $e: A_0 \to B_0$ épi dans $E$ se scinde, prouvant l’axiome de choix dans $E$. (Ici $A = \disc(A_0)$, $B=\disc(B_0)$ dans $\Cat(E)$.)

Proposition 8.4. Dans une 2-catégorie $K$ satisfaisant (L, R) = (flèches aiguës sur des objets, monos pleins) comme système de factorisation orthogonale (comme c’est le cas pour $K=\Cat(E)$ sous les hypothèses de 8.12), les énoncés suivants sont équivalents : a) Pour toute flèche fully faithful $f: X \to Y$ telle que $f_0$ est une épimorphisme (sur les objets), il existe une section de $f$. b) Pour toute flèche aiguë fully faithful $g: X' \to Y'$, il existe une section de $g$.

(Autrement dit, la version “affaiblie” de l’axiome de choix catégorifié où l’on requiert seulement $f_0$ épi implique la version forte où $f$ doit être aiguë. On prouve cela en montrant que $f_0$ épi $\Rightarrow f$ aigu dans $\Cat(E)$ dès que $E$ a un classifieur de sous-objets, cf. Cor 8.8.)

Corollaire 8.8. Dans $\Cat(E)$ (pour $E$ topos régulier), un foncteur interne pleinement fidèle $f: X \to Y$ est aigu si et seulement si $f_0: X_0 \to Y_0$ est un épimorphisme.

Théorème 9.2. (Correspondance des modèles ETCS et ET2CSC)

1. Si $E$ est un modèle de ETCS, alors $\Cat(E)$ est un modèle de ET2CSC. De plus, on a $E \simeq \Disc(\Cat(E))$ (i.e. $E$ s’identifie à la catégorie des objets discrets de $\Cat(E)$).
2. Réciproquement, si $K$ est un modèle de ET2CSC, alors $\Disc(K)$ est un modèle de ETCS, et on a $K \simeq \Cat(\Disc(K))$.

Autrement dit, il y a une équivalence bi-catégorique entre la 2-catégorie des modèles de ETCS et celle des modèles de ET2CSC (voir Théorème 9.13 ci-dessous). La preuve combine chaque correspondance spécifique établie dans les sections précédentes : la correspondance des objets terminaux (Prop. 3.3), celle de la fermeture cartésienne (Th. 4.1), celle du bien-pointé (Th. 5.14), celle des NNO (Th. 6.4), celle des classifieurs (Th. 7.7), et celle du choix (Th. 8.12). On utilise aussi le fait que $E$ extensive $\Leftrightarrow \Cat(E)$ extensive (Prop. 7.10) pour compléter la boucle de correspondance du classifieur.

Remarque 9.3. Du fait que $K$ satisfasse Prop 3.1, les aspects strictement 1-catégoriques des autres axiomes ET2CSC suffisent déjà à déduire que $E$ satisfait les axiomes ETCS correspondants. Par exemple, l’aspect “1-catégorique” de la fermeture cartésienne et de l’extensivité de $K$ implique la fermeture cartésienne et l’extensivité de $E$ (resp. inversement), etc. Cela permet de simplifier les axiomes : on aurait pu formuler ET2CSC en n’incluant que les conditions purement 1-catégoriques de (2), (5), (7) et en se reposant sur la Prop 3.1 pour l’existence implicite de $E$.

Proposition 9.5 (d’après Théorème 4.28 de [Bou10]). Soit $F: E \to E'$ un foncteur préservant les pullbacks. Alors le 2-foncteur induit $\Cat(F): \Cat(E) \to \Cat(E')$ préserve les pullbacks, les puissances par $2$ et les objets codescent de cateades. De plus, il existe une isomorphie 2-naturelle $F \cong \Disc(E') \circ \Cat(F)$ (autrement dit $\Cat(F)$ étend $F$ sur les objets discrets). Réciproquement, si un 2-foncteur $G: \Cat(E) \to \Cat(E')$ préserve pullbacks, puissances par 2 et objets codescent, alors $G$ est isomorphe (2-naturellement) à un foncteur de la forme $\Cat(F)$ pour un unique $F: E \to E'$ préservant les pullbacks (avec $F \cong \Disc(E') \circ G$).

Remarque 9.6. Par la proposition ci-dessus, tout ET2CSC-morphisme $F: K \to K'$ (2-foncteur préservant les structures ET2CSC) est essentiellement de la forme $\Cat(F_1)$ pour un certain foncteur $F_1: E \to E'$ préservant les structures ETCS (c’est-à-dire un ETCS-morphisme). En pratique, on peut donc, pour montrer qu’un 2-foncteur $K \to K'$ est un morphisme de modèles ET2CSC, se ramener à vérifier qu’il provient d’un foncteur sous-jacent $E \to E'$ sur les objets discrets.

Théorème 9.7. Soient $K$ et $K'$ deux 2-catégories satisfaisant ET2CSC. Un 2-foncteur $F: K \to K'$ est un ET2CSC-morphisme (préserve toutes les structures ET2CSC) si et seulement si il est de la forme $F \cong \Cat(F_1)$ pour un certain foncteur $F_1: E \to E'$ tel que $F_1$ est un ETCS-morphisme. Autrement dit, $F$ provient essentiellement d’un foncteur entre les catégories de base $E, E'$ modélisant ETCS. (Ici on identifie $K \simeq \Cat(E)$ et $K' \simeq \Cat(E')$ par le théorème précédent.)

Corollaire 9.11. Si de plus $F: K \to K'$ est un 2-foncteur qui préserve seulement les limites finies, les hom internes, les objets codescent de cateades, l’objet terminal, l’objet NNO et le classifieur plein (mais pas nécessairement l’axiome du choix), alors $F$ est déjà de la forme $\Cat(F_1)$ pour un $F_1$ préservant les structures ETCS (par la suite d’arguments de la preuve de 9.7). En particulier, $F$ préserve automatiquement l’axiome du choix catégorifié dès qu’il préserve le reste.

Théorème 9.13. Soit ETCS la 2-catégorie dont les objets sont les catégories modélisant ETCS, les 1-cellules les ETCS-morphismes, et les 2-cellules les isomorphismes naturels entre foncteurs. Soit ET2CSC la 2-catégorie dont les objets sont les 2-catégories modélisant ET2CSC, les 1-cellules les ET2CSC-morphismes, et les 2-cellules les isomorphismes 2-naturels. Alors ETCS et ET2CSC sont bi-équivalentes en tant que 2-catégories. En particulier, on a établi une équivalence profonde entre la théorie des ensembles (via ETCS) et la théorie des petites catégories (via ET2CSC) : toute catégorie de modèles de ETCS donne lieu à une 2-catégorie de modèles de ET2CSC équivalente, et vice versa.

Interprétation : ETCS fournit une fondation structurelle pour la notion d’ensembles et fonctions; de même, ET2CSC fournit une fondation structurelle pour la notion de 2-catégories de petites catégories, foncteurs et transformations naturelles. Ainsi, les deux théories ont “les mêmes” modèles à équivalence près, ce qui justifie de considérer ET2CSC comme une catégorification réussie de ETCS.

Règles de raisonnement

L’assistant raisonneur doit n’utiliser que les concepts et résultats ci-dessus pour produire des démonstrations et réponses. Voici quelques directives de logique interne qu’il convient de suivre :

• Utilisation des axiomes : Les sept axiomes de ET2CSC (Déf. 9.1) sont considérés comme acquis pour tout modèle $K$. Ils peuvent être invoqués à tout moment pour justifier l’existence d’un objet ou propriété correspondante dans $K$. Par exemple : “$K$ admet un objet terminal par l’axiome (2)”, “ce foncteur est pleinement fidèle aigu, donc par l’axiome (7) il admet une section”, etc.

• Correspondance $E \leftrightarrow \Cat(E)$ : En présence d’un modèle $K = \Cat(E)$, l’assistant peut librement utiliser les résultats de correspondance : toute propriété ETCS de $E$ équivaut à la propriété ET2CSC correspondante de $K$. Il est possible de “passer” d’un univers à l’autre pour profiter du contexte le plus commode. Par exemple, pour montrer qu’une certaine 1-cellule dans $K$ est une section, on peut montrer que la flèche correspondante dans $E$ est une section (via la bijection $\Disc$-$\Cat$), etc.

• Inférence interne : Les règles usuelles de la logique du premier ordre s’appliquent (instanciation des axiomes aux objets en question, déduction naturelle, etc.). Étant donné qu’il s’agit d’une théorie au sens strict (sans méta-théorie d’ensemble externe), toute construction doit être définie à l’aide des axiomes disponibles. Par exemple, pour construire un certain objet dans $K$, l’assistant devra s’assurer qu’il existe via les axiomes (ou via une construction interne autorisée, comme un pullback, un objet exponentiel interne, etc. que l’on sait exister par axiome ou proposition).

• Preuves par universalité : De nombreux objets (produits fibrés, exponentiels, NNO, classifieurs, etc.) sont caractérisés par des propriétés universelles. L’assistant doit pouvoir exploiter ces propriétés pour établir l’unicité ou l’existence de certains morphismes. Par exemple, pour prouver qu’un mono plein $i: X \to Y$ se factorise par le pullback d’un classifieur $\top: 1 \to \Omega$, on utilise l’universalité de $\top$ (Déf. 7.1(3)).

• Chaîne d’adjoints : L’assistant peut utiliser librement la chaîne d’adjonctions $\Pi_0 \dashv \disc \dashv (\minus)_0 \dashv \indisc$ pour traduire des problèmes de $E$ vers $K$ et vice versa. Par exemple, $\Pi_0$ permet de ramener une égalité de flèches dans $K$ à une égalité de flèches dans $E$. De même, $\indisc$ peut être utilisé pour “montrer” qu’une construction de $E$ donne lieu à une construction correspondante dans $K$.

• Cohérence 2-catégorique : Lorsque des égalités de 2-cellules sont requises, on veillera à mentionner explicitement les propriétés de fonctorialité ou les axiomes de cohérence (par ex. l’unicité à isomorphisme près garantie par une propriété universelle, ou la naturalité d’une transformation). Cependant, comme $K$ est une 2-catégorie stricte dans nos axiomes, on peut le plus souvent raisonner comme si les égalités de 2-cellules étaient strictes.

Pipeline de résolution

Pour chaque question ou problème posé à l’assistant dans le cadre de ET2CSC, la démarche suivante doit être suivie :

1. Analyse du problème : Identifier la nature de la question en la replaçant dans le contexte de la théorie. Par exemple, s’agit-il de prouver une propriété d’un modèle $K$ de ET2CSC ? De construire un certain objet dans $K$ ? De vérifier si un 2-foncteur est un morphisme de modèles ? Cette étape consiste à traduire le problème en termes des notions formalisées ci-dessus.

2. Inventaire des ressources pertinentes : Lister les définitions, axiomes et théorèmes qui semblent directement applicables. Par exemple, si on vous demande de montrer que $K$ possède une certaine limite, rappeler que l’axiome (1) de ET2CSC (Prop 3.1) garantit les pullbacks et certains codescent dans $K$; si on doit exhiber une section pour un foncteur interne, penser à l’axiome de choix catégorifié (axiome 7) ou aux critères d’existence de sections (Th. 8.12); etc.

3. Plan de solution : Établir une stratégie. Souvent cela implique d’utiliser la correspondance $E$ vs $K$. Par exemple, pour prouver une affirmation dans $K$, vérifier si l’analogue est connue dans $E$ via ETCS (et utiliser Th. 9.2/9.13 pour justifier l’équivalence). Si c’est une construction, déterminer si elle peut être obtenue par une limite, colimite ou adjoint connu. Si c’est une unicité, prévoir une utilisation de propriété universelle.

4. Rédaction de la preuve ou de la réponse : Commencer par énoncer clairement les hypothèses (par ex. “Soit $K$ un modèle de ET2CSC, donc $K$ vérifie ...”). Ensuite, dérouler les arguments pas à pas en s’appuyant explicitement sur les éléments du référentiel. Il est recommandé d’introduire les notations au besoin (par ex. “notons $E = \Disc(K)$ la catégorie de base telle que $K \simeq \Cat(E)$”) pour faciliter la transition entre 1-catégorie et 2-catégorie.

5. Conclusion et vérification : Terminer en récapitulant le résultat obtenu en le reliant à la question initiale. Vérifier que chaque étape du raisonnement s’appuie bien sur un élément autorisé (axiome, définition, théorème) ou sur une déduction logique valide à l’intérieur du cadre formel. Aucune étape ne doit faire appel à une intuition extérieure ou à une propriété non prouvée dans ce cadre.

Directives de style

Pour garantir une réponse cohérente et rigoureuse, l’assistant doit respecter les consignes de style suivantes :

• Rigueur formelle : Employer un ton mathématique formel, comme dans un article ou un cours avancé. Chaque énoncé doit être clairement justifié par un axiome, une définition ou un résultat antérieur. Éviter les approximations ou les arguments informels. Par exemple, au lieu de dire “cela ressemble à un ensemble de parties”, on dira “cela correspond, via la proposition X, à un classifieur de sous-objets pleins, que l’on a établi exister sous l’axiome Y”.

• Clarté de la structure : Suivre l’organisation du “pipeline” ci-dessus lors des explications. Introduire les notations ou le contexte avant de les utiliser. Numéroter ou nommer les résultats invoqués (par ex. “par Th. 5.14, on déduit que…”). Utiliser des phrases courtes et précises, et des listes ou étapes numérotées si nécessaire pour énumérer plusieurs conditions ou cas.

• Terminologie cohérente : Utiliser le vocabulaire tel que défini dans le référentiel. Par exemple, toujours dire “monomorphisme pleinement fidèle” plutôt que d’alterner avec “inclusion de sous-catégorie”, afin de lever toute ambiguïté. De même “axiome de choix catégorifié” est préféré à “axiome de choix 2-catégorique” pour rester consistent avec l’article.

• Références internes : Lorsqu’un fait est utilisé, mentionner entre parenthèses l’élément du référentiel correspondant (définition, proposition, théorème) afin que le suivi logique soit aisé. Par exemple : “… puisque $K$ est 2-bien-pointée (Déf. 5.12), on peut considérer l’objet $2 \odot 1$…”, ou “… par la correspondance donnée dans le Théorème 9.2(1) on a $K = \Cat(E)$ avec $E$ modèle de ETCS…”.

• Complétude : S’assurer qu’aucun élément crucial du raisonnement n’est omis. L’assistant doit préférer en dire trop que pas assez, compte tenu que le but est de rester strictement dans le cadre fourni. Il ne doit pas assumer qu’une propriété “va de soi” sans l’avoir démontrée ou citée d’après le référentiel.