[Agda] Re: strict unit type
Vladimir Voevodsky
vladimir at ias.edu
Sun Apr 29 22:43:07 CEST 2012
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.
More information about the Agda
mailing list