A.2 The second presentation

In this section, there are three kinds of judgments {mathpar} Γ $\mathsf{ctx}$ Γ ⊢a : A Γ ⊢a ≡a’ : A which we specify by providing inference rules for deriving them. A typical inference rule has the form

$\inferrule*[right=\textsc{Name}]{\mathcal{J}_{1}\\ \cdots\\ \mathcal{J}_{k}}{\mathcal{J}}$

It says that we may derive the conclusion $\mathcal{J}$ , provided that we have already derived the hypotheses $\mathcal{J}_{1},\ldots,\mathcal{J}_{k}$ . (Note that, being judgments rather than types, these are not hypotheses internal to the type theory in the sense of §1.1 (http://planetmath.org/11typetheoryversussettheory); they are instead hypotheses in the deductive system, i.e. the metatheory.) On the right we write the Name of the rule, and there may be extra side conditions that need to be checked before the rule is applicable.

A derivation of a judgment is a tree constructed from such inference rules, with the judgment at the root of the tree. For example, with the rules given below, the following is a derivation of $\cdot\vdash{\lambda}x.\,x:\mathbf{1}\to\mathbf{1}$ . {mathpar} \inferrule*[right= $\Pi$ -intro] \inferrule*[right= $\mathsf{Vble}$ ] \inferrule*[right= $\mathsf{ctx}$ -ext] \inferrule*[right= $\mathbf{1}$ -form] \inferrule*[right= $\mathsf{ctx}$ -emp] $\cdot$ $\mathsf{ctx}$ ⊢ $\mathbf{1}$ : $\mathcal{U}$ _0 x : $\mathbf{1}$ $\mathsf{ctx}$ x : $\mathbf{1}$ ⊢x : $\mathbf{1}$ $\cdot$ ⊢λx. x : $\mathbf{1}$ → $\mathbf{1}$

Title	A.2 The second presentation
\metatable