[Agda] Re: strict unit type

[Vladimir Voevodsky]

On Apr 30, 2012, at 9:23 AM, Andreas Abel wrote:

>> 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.
> 
> Such a reduction is unhealthy except in the situation where \prod is a "for all" that does not leave marks on the term level.

Well, that was my first thought as well but I am not so sure now. It does make it necessary to do some type checking before beta-reduction but anyhow the reduction such as a -> tt for objects of the unit type makes reduction context dependent. I have not checked all the details yet but it is possible that one can preserve confluence and normal form and still have reductions which change the sum/prod-structure of type expressions. 

Vladimir.

PS From the point of view of a user who wants to construct/verify proofs the more identifications are recognized by the underlying system the better.