''$\Gamma\vdash A\ \textrm{true}$'' in Martin-Löf type theory

Question

I have a basic question about the notation ''$\Gamma\vdash A\ \textrm{true}$'' in Martin-Löf type theory. In his 1984 book, Martin-Löf says that if we have $\Gamma\vdash a:A$ and we do not care about the computational content of the proof, we shall suppress $a$ writing simply $\Gamma\vdash A\ \textrm{true}$. My question is, what is ''true'' in this notation? Is ''true'' a type, or is it a meta-level label?

Answer 1

"$\Gamma \vdash A\text{ true}$" is a judgment, which we can read as "in the context $\Gamma$ the proposition $A$ is true".

You've already encountered another sort of judgment, "$\Gamma \vdash a : A$", which we normally read as "in the context $\Gamma$, the term $a$ has type $A$", or under the identification of propositions and types, "in the context $\Gamma$, the term $a$ proves the proposition $A$".

The label $\text{ true}$ belongs to the same syntactic category in the former judgment that the turnstile symbol "$\vdash$" and the colon symbol "$:$" belong to in the latter judgment. They form part of the notation that we use for writing judgments.