# Ref request: modelling regular theories as an injectivity condition

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.



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.

• I've used the converse of this – that injectivity conditions are regular sequents – in my paper on internal homotopy theory. – Zhen Lin Feb 3 '16 at 12:45
• @ZhenLin: ah, thankyou! Henrik Forssell also pointed out to me that the same converse appears in the Adamek/Rosicky book, in the hint to Exercise 5.e. These would be close enough to serve as a reference if there’s nothing closer, but it would be nice to have this version itself if it’s been set down somewhere. – Peter LeFanu Lumsdaine Feb 3 '16 at 13:38
• This is a special case of Remark 5.33 in my book with Adámek which deals with small cone injectivity. – Jiří Rosický Feb 6 '16 at 9:07