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

*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****H**>>**t**in**T****H**>>**t**in**T****H**>>**t**= in**T***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".

Thu Sep 14 08:45:18 EDT 1995