Internal Language of a Model

Abstract

In Uemura’s sense, the internal language of a model is the type theory obtained by allowing the objects and elements already present in a model to be used as formal symbols. If $\mathcal{T}$ is a type theory and $\mathcal{M}$ is a model of $\mathcal{T}$, then the internal language $L(\mathcal{M})$ is a theory over $\mathcal{T}$: it keeps the rules of $\mathcal{T}$ while adjoining constants and axioms corresponding to semantic data in $\mathcal{M}$.

A judgment derivable in $L(\mathcal{M})$ can therefore be interpreted back as an actual construction or equality in the model. The point is that one can reason syntactically inside the internal language instead of repeatedly constructing semantic data by large commuting diagrams.

Definition

Formally, a type theory $\mathcal{T}$ is a category with representable maps, while a model $\mathcal{M}$ is a suitable structure-preserving functor from $\mathcal{T}$ into discrete fibrations over a base category $\mathcal{M}(\diamond )$.

For each object $A$ of $\mathcal{T}$, the internal language takes the fibre over the terminal object $1$ of the discrete fibration $\mathcal{M}(A)$. Equivalently, it records the global elements of each semantic object:

$L(\mathcal{M})(A):=\mathcal{M}(A{)}_1$

This produces a left-exact functor $L(\mathcal{M}):\mathcal{T}\to \mathbf{Set}$, hence a $\mathcal{T}$-theory. Uemura writes this construction as a functor

$L:\mathrm{Mod}(\mathcal{T})\to \mathrm{Th}(\mathcal{T})$

He then shows that $L$ yields an equivalence between theories over $\mathcal{T}$ and democratic models of $\mathcal{T}$. For that class of models, passing from syntax to semantics and then extracting the internal language loses no essential information.

Interpretation

Concretely, in a model of dependent type theory:

• A semantic type $A$ becomes a type constant in the internal language.
• A semantic section $a:A$ becomes a term constant.
• An equality between semantic sections becomes a derivable equality axiom.

If the model supports $\Pi$-types, identity types, universes, or other constructors, the internal language lets one use those constructors to build new semantic objects and prove properties of them.

Comparison

This notion is related to, but not identical with, the internal language of a topos or of a presheaf category. That more familiar notion is usually a higher-order or simply typed language in which objects of the topos are types and morphisms are terms.

Uemura uses that notion when reasoning inside a topos of presheaves, but his main notion is more general: it is the dependent type-theoretic language extracted from an arbitrary model of an arbitrary abstract type theory.