[TYPES] strict unit type

[Frederic Blanqui]

Hello.

I just realized that there may be another problem with rule 2. If rule 2 
is included as is in the usual type conversion (conv) used in dependent 
type systems

(conv) if t:T, T\equiv T' and T':s, then t:T',

then you get that:

\lambda x:nat.Pt is of type \Pi x:bool.Pt
since \Pi x:nat.Pt \equiv Pt \equiv \Pi:bool. Pt.

And, to prove the subject reduction property for beta ((\lambda x:T.u)t 
-> u{x=t}), one usually first check the "injectivity" of \Pi wrt \equiv:

\Pi x:A.B \equiv \Pi x:A'.B' implies A\equiv A' and B\equiv B'

This cannot be the case (nat\not\equiv bool) if you add rule 2 in \equiv .

So, could you make more precise what you mean by adding these rules in a 
dependent type system?

Frederic.

Le 01/05/2012 21:18, Vladimir Voevodsky a écrit :
> 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.