[TYPES] strict unit type

[Frederic Blanqui]

Le 30/04/2012 21:04, Vladimir Voevodsky a écrit :
> On Apr 29, 2012, at 8:27 PM, Frederic Blanqui wrote:
>
>> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>>
>> Hello Vladimir.
>>
>> Le 29/04/2012 22:10, Vladimir Voevodsky a écrit :
>>> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>>>
>>> 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 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,
>> This has been done already with this reduction rule. Please, check the work of Roberto Di Cosmo and Delia Kesner for instance.
>>
>>> 2. Prod x : T , Pt reduces to Pt,
>>>
>>> 3. Prod x : Pt , T reduces to T.
>> On the other hand, I am not sure that these rules have been considered yet since, by doing so, you may well loose the property that reduction preserves typing: if t : T reduces to u, then u : T (a property often called "subject reduction"). Unless perhaps if you consider the following extra rules:
>>
>> 2'. (\lambda x:T. t) reduces to tt if t : Pt,
>>
>> 3'. (\lambda x:Pt, t) reduces to t{x=tt}.
> Yes, I did. But also this would follow from the previous 3 rules. For example  (\lambda x:T. t) for t:Pt will have the type, in normal form, Pt and therefore will be reducible to tt by the first reduction.
>
> Vladimir.
>
>
>
Yes, 2' is a consequence of 2 & 1. But I do not see why 3' is a 
consequence of the other rules. By 1, you have (\lambda x:Pt. t) reduces 
to (\lambda x:Pt. t{x=tt}). Then, how to remove (\lambda x:Pt)?

But, after all, it may not be necessary to consider this extra rule. I 
was thinking that having term-level rules corresponding to your 
type-level rules could help, but I am not sure anymore. It may well work 
fine to consider types up to your equivalence relation.

On the other hand, there is a little problem with rule 3 in case x 
occurs free in T. You should instead consider:

3. (Prod x:Pt, T) reduces to T{x=tt}.

Frederic.