The Coq mailing list

[Bruno Barras <bruno.barras AT inria.fr>]

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.

> 
>> 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!)

> 
>> 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.

Bruno.