A.2 The second presentation

In this section, there are three kinds of judgmentsΓ $\mathrm{𝖼𝗍𝗑}$Γ ⊢a : AΓ ⊢a ≡a’ : Awhich we specify by providing inference rules for deriving them. A typical inference rulehas the form

$$*[right=\mathrm{\text{Name}}]{𝒥}_1\mathrm{\cdots }{𝒥}_k𝒥$$

It says that we may derive the conclusion $𝒥$, provided that we havealready derived the hypotheses ${𝒥}_1,\mathrm{\dots },{𝒥}_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 theright we write the Name of the rule, and there may be extra side conditions thatneed to be checked before the rule is applicable.

A derivationof a judgment is a tree constructed from such inferencerules, with the judgment at the root of the tree. For example, with the rules given below, the following is a derivation of$\cdot ⊢\lambda x.x:\mathrm{𝟏}\to \mathrm{𝟏}$.*[right=$\mathrm{\Pi }$-intro]*[right=$\mathrm{𝖵𝖻𝗅𝖾}$]*[right=$\mathrm{𝖼𝗍𝗑}$-ext]*[right=$\mathrm{𝟏}$-form]*[right=$\mathrm{𝖼𝗍𝗑}$-emp] $\cdot$ $\mathrm{𝖼𝗍𝗑}$ ⊢$\mathrm{𝟏}$ : $𝒰$ _0x : $\mathrm{𝟏}$ $\mathrm{𝖼𝗍𝗑}$x : $\mathrm{𝟏}$ ⊢x : $\mathrm{𝟏}$$\cdot$ ⊢λx. x : $\mathrm{𝟏}$ →$\mathrm{𝟏}$