Catégorie syntaxique

Qu'est-ce que tu sais déjà, qu'est-ce que tu ne sais pas, qu'est-ce qui te gêne ?

Un contexte c'est essentiellement une déclaration de variables.

Quand tu fais une preuve mathématique, disons d'analyse, tu diras des choses comme "Soit $x$ un nombre réel, $\epsilon $ un réel strictement positif vérifiant telle chose par rapport à $x$" etc.
En théorie des types, ces déclarations "soit machin" deviennent le contexte, ainsi tu pourras avoir un contexte $\Gamma$ qui vaut $x: \mathbb R, \epsilon : \{y : \mathbb R_+^*\mid y > \frac{1}{|x|+1}\}$ par exemple (remarque qu'ici le deuxième type dépend de $x$, mais on pourrait très bien aussi avoir par exemple $x:\mathbb R, \epsilon : \mathbb R_+^*$, etc. ).

Une fois que tu as ça, un morphisme entre contextes est défini dans la page en question : disons que tu as deux contextes $\Gamma,\Delta$, alors un morphisme $\Gamma\to \Delta$ ce sera une manière de déclarer le contexte $\Delta$ à partir de celui de $\Gamma$.

Par exemple, disons que tu pars juste de $\Gamma := (x: \mathbb R)$, et que tu veux trouver un $0<\epsilon < \frac{1}{|x|+1}$, bah ce sera représenté par un morphisme $\Gamma \to (x:\mathbb R, \epsilon : \mathbb R_+^*, \epsilon < \frac{1}{|x|+1})$, avec, par exemple $\Gamma \vdash x: \mathbb R, \Gamma\vdash \frac{1}{|x|+2} : \{y: \mathbb R_+^*\mid y< \frac{1}{|x|+1}\}$.

Il y a plein d'autres morphismes, mais si tu veux un morphisme $\Gamma\to \Delta$ c'est une manière d'interpréter le contexte $\Delta$ en partant de $\Gamma$.

Donc en résumé : un contexte c'est une liste de déclarations de variables et d'où elles habitent (j'espère que ça rend le nom "contexte" plus clair : c'est en gros le contexte de ta preuve - "dans cette preuve on aura telles et telles variables, c'est le contexte dans lequel je travaille"); et un morphisme de contextes c'est une manière de passer d'un contexte à un autre, c'est-à-dire de définir des variables qui correspondent au second contexte en partant des variables du premier contexte.

Bah bien sûr, une théorie a des types et des axiomes, sinon la catégorie syntaxique ne dépendrait pas de la théorie :-S

Par exemple (celui qui est pris sur le nLab), avec les groupes, tu veux qu'un modèle de ta théorie soit un groupe, il te faut bien des axiomes pour cela.

Un terme est défini dans un contexte. Par exemple, dans la théorie des groupes, tu pourras avoir le terme $xy$ dans le contexte $x:G,y:G,z: G$, mais pas dans le contexte $x:G$ (qui est $y$ ???)
Un terme est un machin que tu peux construire avec des variables et avec les fonctions élémentaires de ta théorie (dans le cas des groupes : la multiplication, l'inverse, le neutre); chaque variable étant déclarée dans ton contexte et étant d'un type fixé.

"Comment savoir quand deux morphismes sont égaux ?" : c'est une très bonne question, ça va un peu dépendre des présentations. Souvent on dit que deux morphismes sont égaux quand les termes qui les constituent sont prouvablement (au sens de la théorie) égaux dans le contexte donné.

Par exemple, dans la théorie des groupes, tu prends $\Gamma := (x:G, y:G,z:G)$ et $\Delta := (a:G)$, alors tu as en particulier deux morphismes $\Gamma \to \Delta$ définis par les termes $(xy)z$ et $x(yz)$. Ces deux-là sont prouvablement égaux, donc les morphismes correspondants aussi.
En particulier, la question de savoir quand deux morphismes sont égaux n'est pas évidente (rien que dans la théorie des groupes, cf. l'indécidabilité du word problem)

Pour une première excursion vers les topos classifiants (même si c'en est encore bien loin - mais je pense que c'est une étape nécessaire), je te conseille de lire l'interprétation d'Awodey des idées de Lawvere, ici (c'est le chapitre 1).
Faut dire que Lawvere a développé ces idées pendant sa thèse, elle est vraiment géniale (aujourd'hui c'est des trucs relativement basiques, mais il faut penser à l'époque !!), et donne les idées essentielles de la sémantique fonctorielle (c'est son titre d'ailleurs), qui est à la base de la théorie des topos classifiants.
Je pense qu'une fois que tu auras compris cette idée dans le cas relativement simple des théories algébriques, tu seras mieux armé pour attaquer des théories plus complexes (notamment typées), et donc à terme les topos classifiants.