[Agda] Re: [TYPES] strict unit type

[Vladimir Voevodsky]

On May 1, 2012, at 5:24 AM, Altenkirch Thorsten wrote:

> In general we shouldn't expect to decide eta equality by untyped
> reduction. eta equality isa form of decidable extensionality and does not
> correspond well to computation to a normal form.
> 
> Clearly, the case of the unit type shows that we need to know the type to
> check equality.
> 
> Trying to decide eta equalities by reduction is very non-modular. This is
> basically the point of Vladimir's email.
> 
> However, if we implement it as a type directed decision procedure things
> are much better. E.g. to terms f,g : Pi x:A.B x are convertible if f x and
> g x : B x are convertible (whewre x is a fresh variable) after beta
> reduction. Similarily, two terms p,q : Sigma x:A.B x are convertible if
> p.1 and q.1 : A are convertible after beta reduction and p.2 and q.2 : B
> p.1 (or B q.1) are convertible after beta reduction. (The and here has to
> be read sequentially, and the choice B p.1 or B p.2 actually causes some
> technical problems).

Why just after beta reduction and not say iota-reduction or even some internal eta-reduction?

Vladimir.