[Agda] Re: strict unit type

[Vladimir Voevodsky]

Thanks for a detailed explanation!

I guess the problem with expansion instead of reduction is that it is non-terminating (e.g. in the case of dependent sums or lambda's) and the condition that one is allowed to apply expansion only once, it seems to me, should complicate rigorous meta-theory a lot.

Vladimir.


PS There is another non-confluent situation with a -> tt for a : Pt which does not require dependent sums namely \lambda x:T, f x where f : T -> Pt reduces both to f and to \lambda x:T tt . Both non-confluences can be taken care of by additional reductions in particular the reduction \prod x:T, Pt -> Pt for the example with \lambda. 





  
On Apr 29, 2012, at 5:36 PM, Guillaume Brunerie wrote:

> 2012/4/29 Vladimir Voevodsky <vladimir at ias.edu>:
>> 
>> On Apr 29, 2012, at 12:36 PM, Guillaume Brunerie wrote:
>> 
>>>>>> 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 is just the eta-expansion rule for Pt. For example Agda has it if
>>>>> you implement Pt as a record.
>>>>> You only need this (and beta/iota reduction) for (Pt) to be terminal
>>>>> in the category of contexts (it will be isomorphic to the empty
>>>>> context).
>>>> 
>>>> I wonder how it works in Agda. This reduction for the unit type creates non-confluet situation when combined with iota/eta reduction for dependent sums. Additional reductions are needed to recover confluence. Are they implemented in Agda?
>>> 
>>> Do you have an example of a problematic situation?
>>> By the way, I am far from a specialist in Agda, but perhaps that
>>> normalization is implemented with something like normalization by
>>> evaluation, which does not require confluence (I think).
>> 
>> For c: \sum x : Pt, Y the term [pair]([pr1](c), [pr2](c)) reduces both to c and to [pair](tt, [pr2](c)) and these two terms can not be reduced to a common term unles a special reduction rule is introduced for this.
>> 
>> V.
> 
> Eta-conversion is usually seen as an expansion rule, it’s c that
> "reduces" to [pair]([pr1](c), [pr2](c)) and not the other way around.
> In your example, everything reduces to [pair](tt, [pr2](c)) and there
> is no problem of confluence.
> Do you have another example which would still be a problem with this
> eta-expansion rule?
> 
> Similarly, for functions the eta-expansion rule reduces f to \lambda x
> . f x (you have to make sure that f has not already been eta-expanded,
> I don’t remember exactly how).
> This makes sense because the purpose of eta-expansion is to convert
> terms to canonical inhabitants of their type. A canonical inhabitant
> of Pt is tt, so eta-expansion convert u : Pt to tt, a canonical
> inhabitant of \sum x : A, P x is a pair, so eta-expansion expands a
> term into a pair, and a canonical inhabitant of a function type is a
> \lambda abstraction.
> Also, normalization by evaluation always gives beta-reduced
> eta-expanded normal forms.
> 
> I’m not sure how Agda works, though. I tried a few things, and in the
> context (u : unit), the normal form of u is u, but refl u is
> nevertheless accepted as an inhabitant of the identity type Id unit u
> tt, so it seems that convertibility is not defined as equality of
> normal forms in Agda.
> 
> Guillaume