[Agda] Re: strict unit type

[Guillaume Brunerie]

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