For each of the type constructors of the theory there are two introduction rules, one of the form H >> A and one of the form H >> a in A. For instance, we have
and>>
|
by intro at
right
>>
>>
in
These rules have essentially the same content to the extent that the judgements are completely reflected in the equality types, but the former leaves the inhabiting object, inl(a), suppressed whereas the latter treats it explicitly. In the first rule the extracted object is inl(a), while in the latter it is the token axiom. Intuitively, the first of the two is useful when we are regarding A|B as the proposition expressing the disjunction of A and B; the latter is useful when we are thinking of A|B as a data type, in which case the right--hand side above expresses the proposition that inl(a) is a member of the type A|B.>> inl(
) in
|
by intro at
>>
in
>>
in
Since types, and hence propositions, are those terms which can be shown to inhabit a universe type, this duality extends to the type (proposition) formation rules --- they are simply the introduction rules for the universe types. Note, however, that the rules are organized in such a way that one does not need to construct a type explicitly before showing it to be inhabited. Each rule is sufficient to show not only that a type is inhabited but also that it is in fact a type. In most cases we go to no special trouble to achieve this, but certain rules contain subgoals whose only purpose is to assist in demonstrating that the consequent is a type. For instance, the second subgoal in the rules above exists solely to ensure that A|B is a type. That A is a type is ensured by the first subgoal; the second provides the additional information necessary to form the union type.
