Internal language

Definition

Let $\mathcal{E}$ be a topos with subobject classifier $\top \colon 1 \to \Omega$, and write $PX$ for the exponential object $\Omega^X$. The internal language (Mitchell–Bénabou language) of $\mathcal{E}$ is the typed language described as follows.

1. The types are the objects of $\mathcal{E}$; the type of a product $X \times Y$ is the product type, and $PX$ is the power type of $X$.
2. There are variables of each type, and each morphism $f \colon X \to Y$ is a function symbol from type $X$ to type $Y$.
3. Terms are built from variables by function symbols and by pairing $\langle \sigma, \tau \rangle$. For terms $\sigma, \tau$ of the same type, $\sigma = \tau$ is a term of type $\Omega$. For $\sigma$ of type $X$ and $\tau$ of type $PX$, the membership $\sigma \in \tau$ is a term of type $\Omega$. For a term $\varphi$ of type $\Omega$, the comprehension $\set{x \in X \mid \varphi}$ is a term of type $PX$.
4. A formula is a term of type $\Omega$.

A term $\tau$ of type $Y$ whose free variables are $x_1 : X_1, \dots, x_n : X_n$ is interpreted as a morphism $X_1 \times \cdots \times X_n \to Y$. Variables are interpreted by projections, function symbols by composition, $\sigma = \tau$ by the characteristic morphism of the diagonal $Y \to Y \times Y$, and $\sigma \in \tau$ by the evaluation morphism $X \times PX \to \Omega$. A formula $\varphi$ is valid in $\mathcal{E}$ when its interpretation equals $\top$ composed with the unique morphism $X_1 \times \cdots \times X_n \to 1$.