[TYPES] strict unit type

[Vladimir Voevodsky]

You are right on both counts. 3' does not follow from 3 and in 3 one has to consider T{x=tt}.

I'll need to check details with how beta reduction should be set up in the presence of 2 and 3 and then it will be clear, I hope, weather 3' is needed.

Vladimir.





On Apr 30, 2012, at 11:10 PM, Frederic Blanqui wrote:

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