The Coq mailing list

[Peter LeFanu Lumsdaine <p.l.lumsdaine AT gmail.com>]

On Mon, Jun 21, 2021 at 12:16 PM Vedran Čačić <veky AT math.hr> wrote:

Is there really a standard model for T_Coq? Is it defined anywhere?

It’s not been worked out for the whole of modern Coq (as far as I know), but it has for various fragments of it, including most of Coq’s individual features.  Of course, “standard model” is a slightly dangerous term — different people mean slightly different things by it.  What I mean here is the sense that the notions in the object theory are interpreted by (nearly) the same notions in the metatheory: types are interpreted roughly just as types or sets — probably “small” or “from some fixed universe”, but not by anything more elaborate like e.g. presheaves, topological spaces, etc..

So yes — “the standard model for Coq” is a somewhat nebulous concept, as indeed is “the type theory of Coq”.  To extract a completely precise statement, you’d need to pick a precisely-defined type theory representing a reasonable fragment of Coq (e.g. CIC).

–p.