[TYPES] strict unit type

[Vladimir Voevodsky]

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.