[Agda] Re: strict unit type

[Vladimir Voevodsky]

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.