Partial types allow the reasoning about partial functions in type theory.  The
partial functions of main interest are recursively computed functions, which are
commonly assigned types using fixpoint induction.  However, fixpoint induction
is valid only on admissible types.  Previous work has shown many types to be
admissible, but has not shown any dependent products to be admissible.
Disallowing recursion on dependent product types substantially reduces the
expressiveness of the logic; for example, it prevents much reasoning about
modules, objects and algebras.

In this paper I present two new tools, predicate-admissibility and monotonicity,
for showing types to be admissible.  These tools show a wide class of types to
be admissible; in particular, they show many dependent products to be
admissible.  This alleviates difficulties in applying partial types to theorem
proving in practice.  I also present a general least upper bound theorem for
fixed points with regard to a computational approximation relation, and show an
elegant application of the theorem to compactness.