The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

On Apr 29, 2012, at 9:41 PM, Bruno Barras wrote:

> On 29/04/2012 17:39, Guillaume Brunerie wrote:
>> Hello,
>> 
>> 2012/4/29 Vladimir Voevodsky 
>>Â <vladimir AT ias.edu>:
>>> Hello,
>>> 
>>> let Pt be the unit type ("one point"). In Coq-like systems it is 
>>> introduced through an eliminator and the associated iota-reduction rule. 
>>> This is in practice sufficient for proving all its expected properties 
>>> modulo propositional equality (or identity types) but does not create a 
>>> terminal object in the category of contexts.
>> 
>> I’m not sure if it is your question, but you do not need a unit type
>> to have a terminal object in the category of contexts, the empty
>> context is already a terminal object (there is exactly one context
>> morphism from any context to the empty context : the empty morphism).
> 
> I think that by category of contexts, Vladimir means a pair (E,T) where
> T is a type in "context" E. The objects are open terms of type T in E.

No, I did mean the usual category of contexts where objects are contexts. And 
yes, I do know that the empty context creates a terminal object. I was just 
making a point that the unit type in Coq does not give a terminal object (and 
dependent sums are not isomorphic to two-step contexts).


> 
>> 
>>> I wonder if any one has considered type theories where Pt is introduced 
>>> as having a distinguished object tt together with reduction rules of the 
>>> following form (in the absence of dependent sums, otherwise one needs 
>>> more):
>>> 
>>> 1. any object of Pt other than tt reduces to tt,
> 
> There's a paper of Abel, Coquand and Pagano: "A modular type-checking
> algorithm for type theory with singleton types and proof-irrelevance",
> which investigates that. Maybe Andreas will give a more precise answer,
> but the conclusion (not only in this paper) is that you cannot do
> agressive reductions without breaking either confluence or strong
> normalization.
> 
> Even in good cases, decidability of conversion needs algorithms
> radically different from what is implemented in Coq. (hence the paper!)


Thanks! I'll look at it.


> 
>> 
>>> 2. Prod x : T , Pt reduces to Pt,
>>> 
>>> 3. Prod x : Pt , T reduces to T.
> 
> I would qualify this as *very* agressive! Extraction, just to mention
> one feature, will not survive this extension.

Unless it is implemented in the target language...

Vladimir.