Organization of the Rules

The rules for reasoning about each type and objects of the type will be presented in separate sections. Recall from above that for each judgement of the form H >> T ext t where the inhabiting object t is left implicit , there is a corresponding explicit judgement H >> t in T ext axiom. As the content of these judgements is essentially the same, the rules for reasoning about them will be presented together. In the preceding chapters, the rules have been classified mainly as introduction or elimination rules, where the introduction rules break down the form of the conclusion of a goal, and the elimination rules use a hypothesis. This is too coarse a classification for the purposes of this section, as the large majority of the rules are introduction rules. Here we will use different criteria for classifying the rules which will hopefully be more illuminating. For each type we will have the following categories  of rules:

• Formation 
  These rules give the conditions under which a canonical type may be judged to inhabit a universe, thus verifying that it is indeed a type.
• Canonical 
  These rules give the conditions under which a canonical object (implicitly or explicitly presented) may be judged to inhabit a canonical type. Note that the formation rules are all actually canonical rules, but it is convenient to separate them.
• Noncanonical 
  These rules give the conditions under which a noncanonical object may be judged to inhabit a type. The elimination rules all fall in this category, as the extract term for an elimination rule is a noncanonical term.
• Equality 
  These rules give the conditions under which objects having the same outer form may be judged to be equal. Recall that the rules are being presented in implicit/explicit pairs, H >> T ext t and H >> t in T. The explicit judgement H >> t in T is simply the reflexive instance of the general equality judgement H >> t = in T, and in most cases the rule for the general form is an obvious generalization of the rule for the reflexive form, and thus will be omitted. As the rules for the reflexive judgement are given in one of the other categories, there will be no equality rules presented for some types.
• Computation 
  These rules allow one to make judgements of equalities resulting from computation.

Rules such as the sequence, hypothesis and lemma rules which are not associated with one particular type are grouped together under the heading "miscellaneous".