[TYPES] strict unit type

[Roberto Di Cosmo]

I am quite happy to see a revival of interest in this subject, and
thanks Frederic for remembering some of the works done in the 1990's
:-)

In case this may be of interest, I had been maintaining a short
history of rewriting with extensionality til 2000, with a brief
summary of the results known then, and of the relevant papers I knew
of by 2000 (this includes some results for CoC too).

It is available as a set of slides here: http://www.dicosmo.org/Slides/Edi99.pdf

Of course, we know more today than what is reported in this short
survey, but I could not help getting interested in a different
research direction, and did not maintain this survey up to date.

If anybody is interested in updating it, I'll be more than happy to
share the LaTeX sources ...

--Roberto

2012/4/30 Frederic Blanqui <frederic.blanqui at inria.fr>:
> [ 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}.
>
> Best regards, Frederic.
>
>> Thanks,
>> Vladimir.



-- 
--Roberto Di Cosmo

------------------------------------------------------------------
Professeur               En delegation a l'INRIA
PPS                      E-mail: roberto at dicosmo.org
Universite Paris Diderot WWW  : http://www.dicosmo.org
Case 7014                Tel  : ++33-(0)1-57 27 92 20
5, Rue Thomas Mann
F-75205 Paris Cedex 13
FRANCE.
------------------------------------------------------------------
Attachments:
   MIME accepted
   Word deprecated, http://www.rfc1149.net/documents/whynotword
------------------------------------------------------------------
Office location:

Bureau 6C15 (6th floor)
175, rue du Chevaleret, XIII
Metro Chevaleret, ligne 6
------------------------------------------------------------------