[Agda] Re: strict unit type

[Andreas Abel]

In Agda eta-expansion is performed only on meta-variables.  Otherwise, 
eta-laws are incorporated into equality checking.  For instance, the query

   p = tt : Pt

for

   record Pt : Set where
     constructor tt

will always succeed, because there is only one inhabitant of Pt.
[ This is why refl : Id u unit succeeds. ]

Similarily,

   pair t1 t2 = c : Sum Pt Y

reduces to the two subqueries

   t1 = pr1 c : Pt
   t2 = pr2 c : Y t1

if Sum is defined as a record.

Cheers,
Andreas

On 29.04.12 11: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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/