[TYPES] strict unit type

[Frederic Blanqui]

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

Best regards, Frederic.

> Thanks,
> Vladimir.