The Coq mailing list

[Peter LeFanu Lumsdaine <p.l.lumsdaine AT gmail.com>]

On Mon, Sep 28, 2015 at 10:20 AM, Vladimir Voevodsky <vladimir AT ias.edu> wrote:

Is it correct to say that the main problem in constructive type theory is to create a type theory that simultaneously satisfies two conditions:

1. the function extensionality principle
2. the principle of decidability of typing judgements

?

Is it right that no such theory exists?

If I remember right, the theory of “intensional type theory with extensional principles”, studied in Martin Hofmann’s thesis, has both of these:

http://www.lfcs.inf.ed.ac.uk/reports/95/ECS-LFCS-95-327/

Specifically, he adds functional extensionality and (propositional) UIP to a core intensional type theory, giving a theory he calls TT_I; and he shows that the induced interpretation from TT_I into extensional type theory (i.e. with the reflection rule) is conservative.  This is Section 3.2.4–5 of the thesis.

On the other hand, TT_I retains decidable type-checking — at least, I recall him showing this, though on a very quick skim, I can’t now find where he does.  (I guess it follows from the decidability of the core intensional type theory, since the extension adds no new definitional equality rules, and so typechecking in the extension reduces to typechecking in a context over the core?)

Best,

–p.