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

>> | by intro at right

>>

>> in

>> 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

`
`

Thu Sep 14 08:45:18 EDT 1995