The Coq mailing list

[Martin Escardo <m.escardo AT cs.bham.ac.uk>]

On 28/09/15 09:42, Bas Spitters wrote:
> Thorsten will write a longer message, but there is OTT, going back to the
> work by Hofmann that Peter mentions:
> http://www.cs.nott.ac.uk/~psztxa/publ/obseqnow.pdf

I would additionally count cubical type theory
http://www.cse.chalmers.se/%7Ecoquand/face.pdf as precisely approaching
this, and more generally propositional and universe extensionality.

Martin


> On Mon, Sep 28, 2015 at 10:39 AM, Peter LeFanu Lumsdaine <
> p.l.lumsdaine AT gmail.com>
>  wrote:
> 
>> 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.
>>
>> --
>> You received this message because you are subscribed to the Google Groups
>> "Homotopy Type Theory" group.
>> To unsubscribe from this group and stop receiving emails from it, send an
>> email to 
>> HomotopyTypeTheory+unsubscribe AT googlegroups.com.
>> For more options, visit https://groups.google.com/d/optout.
>>
> 

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe