The background to the following observation is standard material in categorical logic, and I thought this was was too — I don’t remember learning it, but I don’t think it is original — but I can’t now find it anywhere in the literature. Does it ring a bell to anyone? Even if it is not in print, I would be interested to know if people have heard this discussed informally, to get an idea of which communities this is folklore in.

Recall: a regular formula (over a signature $\Sigma$) is a formula constructed just from atomic formulas, finite conjunction, and existential quantification. $\newcommand{\x}{{\vec x}}\newcommand{\y}{{\vec y}}$Any regular sequent $\varphi(\x) \vdash_\x \psi(\x)$ is derivably equivalent to one in regular normal form, i.e. $\varphi'(\x) \vdash_{\vec x} \exists \y.\ \psi'(\x,\y)$, where $\varphi'$, $\psi'$ are conjunctions of atomics and $\psi'(\x,\y) \vdash_{\x,\y} \varphi'(\x)$ is derivable (this is D1.3.10 in the Elephant).

If $\varphi(\x)$ is any conjunction of atomic formulas, then there is a $\Sigma$-structure $\newcommand{\str}[2]{\langle\!\langle\, #1 \ |\ #2 \,\rangle\!\rangle } \str{\x}{\varphi}$, generated by elements for each variable in $\x$, and with the interpretation just enough to make $\varphi$ hold. This represents the interpretation of $\varphi$: for any other structure $A$, $\newcommand{\Str}{\Sigma\text{-}\mathbf{Str}}\newcommand{\interp}[2]{[\![\, #1 \ |\ #2 \,]\!] } \interp{\x}{\varphi}^A \cong \Str(\str{\x}{\varphi}, A)$.

Then (this is the fact I’m after) a structure validates a regular normal sequent $\varphi(\x) \vdash_{\vec x} \exists \y.\ \psi(\x,\y)$ just if it is injective w.r.t. the obvious map $\str{\x}{\varphi} \to \str{\x,\y}{\psi}$. Correspondingly, being a model of a regular theory $\mathbf{T}$ is a small-injectivity condition.