# A question for Martin-L\"of disciples


The definition of "intensional" Martin-L\"of type theory used
by the Swedes (Nordstr\"om, Petersson, Smith, et al.) in their book
_Programming_in_Martin-L\"of's_Type_Theory_ and Simon Thompson in
_Type_Theory_and_Functional_Programming_ does not look
much like that used by Troelstra and van Dalen in _Constructivism_in_
_Mathematics,_Volume_II_.  The former group eschews the rule IExt:

p : I(A, a, b)
(IExt)	--------------
a = b : A

while the latter cheerfully include it but omit \eta and \xi.

Simon Thompson claims the decidability of judgements [british spelling]
in ML^i; Troelstra and van Dalen seem to make no claim either way about
their system, although there is a cryptic note on page 633 which refers
to the former formulation.

My questions are:

1. Are the two systems "equivalent" (are the sets of theorems in any sense
the same)?
2. If so, how so, and if not, how solvable are judgements in the
Troelstra/van Dalen formulation?