We’ll roughly follow the Elephant and Seely. The following is all entirely standard and here only to fix notation and terminology.

For more details, see these notes.

Type theory

A signature is a collection $X, Y, \ldots$ of sorts, together with function symbols $f \colon \vec X \to Y$ and relation symbols $R \subset \vec X$, where $\vec X$ is a finite list $X_1, X_2, \ldots, X_n$ of sorts, also called a type. We’ll denote types by $X,Y,\ldots$ too.

For each sort $X$ there should be an inexhaustible supply of fresh variables $x$ and bound variables $\xi$ of sort $X$. A context is a finite list $\vec x \colon \vec X$ of sorted variables, or equivalently a single typed variable $x \colon X_1, X_2, \ldots$.

A term is either a variable, a tuple of terms, or an expression of the form $f(t)$ where $f$ is a function symbol and $t$ a term. The free variables of a term are precisely the variables that appear in it. Each term lives in a context, which must contain every variable in the term, perhaps together with ‘dummy’ variables that don’t. We write $t[x]$ to indicate that $x$ is the context of $t$, and $t[s]$ to denote the obvious substitution. The type of a term-in-context is determined in the obvious way: for variables, $x_i[\vec x \colon \vec X] \colon X_i$, while a tuple $(t_1, t_2, \ldots, t_n)[x \colon X] \colon X \to \vec Y$ if each $t_i \colon X \to Y_i$, and $f(t) \colon X \to Y$ if $f \colon Z \to Y$ and $t \colon X \to Z$.

Formulas

The formulas of regular logic are built up from the atomic formulas $R(t)$ (where the type of $t$ is the type of $R$) and $t =_X s$ (where $t$ and $s$ are terms of type $X$) using $\top$ (true), $\wedge$ (conjunction) and $\exists$, where if $\phi[x]$ is a formula then so is $\exists \xi.\phi[\xi]$. The free variables of a formula are defined in the usual way.

The substitution $\phi[t]$ of the term $t$ for the variable $x$ is defined as usual.

Logic

We’ll use the usual natural-deduction rules — conjunction and truth are governed by

existentials by

where on the right $x$ is not free in $\psi$, and equality by

We also have to add the Frobenius axiom $\phi \wedge \exists y. \psi \vdash \exists y.(\phi \wedge \psi)$, where $y$ is not in $\vec x$.

Proofs are considered up to the rewrites given in Seely and Prawitz, together with those making the Frobenius axiom the two-sided inverse to the usual proof of the converse (see e.g. Elephant p. 832). Again, see the notes referenced above.

Models

Models of regular theories are regular fibrations.

If $p \colon E \to B$ is a regular fibration, then an interpretation $I$ of a signature assigns

• to each sort $X$ an object $I X$ of $B$

• to each list $\vec X = X_1, X_2, \ldots, X_n$ of sorts the product $I \vec X = I X_1 \times I X_2 \times \cdots \times I X_n$

• to each function symbol $f \colon \vec X \to Y$ a morphism $I f \colon I \vec X \to I Y$ in $B$

• to each relation symbol $R \subset \vec X$ an object $I R$ in $E_{I \vec X}$ (the fibre of $p$ over $I \vec X$)

Given an interpretation of a signature, terms and formulas over it are given the following meanings:

• $I (x_i[\vec x]) = \pi_i \colon \Pi_j X_j \to X_i$.

• $I f(t_1, t_2, \ldots, t_n) = I f \circ (I t_1, I t_2, \ldots, I t_n)$.

• $I R(t_1, t_2, \ldots, t_n) = (I t_i)_i^* I R$, where $(I t_i)_i$ is the pairing of the meanings of the $t_i$.

• $I(x =_{\vec X} x') = \exists_{\Delta_{I \vec X}} \top$, where $\Delta_{I \vec X} \colon I \vec X \to I \vec X \times I \vec X$ is the diagonal.

• $\top$ and $\wedge$ are interpreted by the finite products in $E$, of course, and $\exists$ by the left adjoints $\exists_\pi$ to product projections $\pi$.

An interpretation $I$ satisfies a sequent $S = \phi \vdash_{\vec x} \psi$, written $I \models S$, if there is a vertical morphism $I \phi \to I \psi$ over $I \vec X$ where $\vec X$ is the sort of $\vec x$.

An interpretation is a model of a theory, written $I \models T$, if it satisfies each sequent contained in the theory.

In the notes referenced above, we see that a regular theory $T$ gives rise to a syntactic model, a regular fibration $E_T \to B_T$. A model of $T$ in $p$ is then a morphism of regular fibrations from $E_T$ to $p$. The following then hold: