  One may formulate the dependent product types of Martin-L\"of type theory
either in terms of abstraction and application operators like those for the
lambda-calculus; or in terms of introduction and elimination rules like those
for the other constructors of type theory. It is known that the latter rules
are at least as strong as the former: we show that they are in fact strictly
stronger. We also show, in the presence of the identity types, that the
elimination rule for dependent products--which is a "higher-order" inference
rule in the sense of Schroeder-Heister--can be reformulated in a first-order
manner. Finally, we consider the principle of function extensionality in type
theory, which asserts that two elements of a dependent product type which are
pointwise propositionally equal, are themselves propositionally equal. We
demonstrate that the usual formulation of this principle fails to verify a
number of very natural propositional equalities; and suggest an alternative
formulation which rectifies this deficiency.
