I'm confused about the introduction of the Mitchell-Bénabou-language in Sheaves in Geometry and Logic:
Here are the inductive clasues which simultaneously define the terms of the language and their interpretation:
- Each variable $x$ of type $X$ is a term of type $X$; its interpretation is the identity $x = 1 : X \to X$.
- Terms $\sigma$ and $\tau$ of types $X$ and $Y$, interpreted by $\sigma : U \to X$ and $\tau : V \to Y$, yield a term $\langle \sigma, \tau \rangle$ of type $X \times Y$; its interpretation is $$ \langle \sigma p, \tau q \rangle : W \to X \times Y,$$ where the source $W$ has evident projections $p : W \to U$ and $q : W \to V$. Here the notation $\langle \quad, \quad \rangle$ is used ambiguously, both for hte new term and for the familiar map into the product $X \times Y$.
- Terms $\sigma : U \to X$ and $\tau : V \to X$ of the same type $X$ yield a term $\sigma = \tau$ of type $\Omega$, interpreted by $$(\sigma = \tau) : W \overset{\langle \sigma p, \tau q \rangle}{\longrightarrow} X \times X \overset{\delta_X}{\longrightarrow} \Omega,$$
In the second point, why not saying $W=U\times V$? Is there a subtle difference between $W$ and $U\times V$ which I'm not seeing right now?
It seems like you've realized the broad reason for this in the comments, but I'll say a quick word about it here.
The domain of our map $\sigma : U \to X$ can be thought of as the context of variables in which $\sigma$ lives. For instance, the term-in-context $x : \mathbb{N}, y : \mathbb{N} \vdash (x+y) : \mathbb{N}$ is interpreted by the arrow $(+) : \mathbb{N} \times \mathbb{N} \to \mathbb{N}$.
Now say we have terms-in-context $x : \mathbb{N} \vdash x+1$ and $x : \mathbb{N} \vdash x+2$. Then there's two natural ways we can interpret the term $\langle x+1, x+2 \rangle : \mathbb{N} \times \mathbb{N}$.
Either, we mean
$$ x : \mathbb{N}, x' : \mathbb{N} \vdash \langle x + 1, x' + 2 \rangle : \mathbb{N} \times \mathbb{N} $$
or we mean
$$ x : \mathbb{N} \vdash \langle x+1, x+2 \rangle : \mathbb{N} $$
First, do you see the difference between these two terms-in-context? And second, do you see how the first is represented by an arrow $\mathbb{N} \times \mathbb{N} \to \mathbb{N} \times \mathbb{N}$ and the second is represented by an arrow $\mathbb{N} \to \mathbb{N} \times \mathbb{N}$? In each case the domain $W$ has natural projections $W \to \mathbb{N}$ and $W \to \mathbb{N}$, it's just that in the second case these projection maps are the same! This is exactly the feature that allows us to stipulate that two variables in a term are "the same", which is an incredibly useful ability to have!
I'll also mention here that while the mitchell-benabou language is extremely useful (read: the syntax is), its interpretation (read: semantics) as defined in Mac Lane and Moerdijk is often less so. Instead, there are alternative semantics defined in the coming sections (namely the kripke-joyal semantics and the special case of sheaf semantics) which are (at least in my experience) easier to work with in practice. I wish Mac Lane and Moerdijk had made it more clear that the various semantics they define are all (roughly equivalent) ways of interpreting the same language. See also the discussion here for more information about this.
I hope this helps ^_^