The Coq mailing list

[Danko Ilik <dankoilik AT gmail.com>]

Hi, and sorry for joining the discussion a bit late,

On Tue, Sep 28, 2021 at 11:18 AM Meven LENNON-BERTRAND <Meven.Bertrand AT univ-nantes.fr> wrote:

The only way out I see, which is how I’ve come to think of those rules, is that they are actually an algorithm for typed conversion, but one that does not maintain types as they are in fact not needed, since for rules η1 and η2 you only need to look at the other side to perform η expansion. In fact, those rules are very close to the ones for algorithmic conversion in Abel et al.’s Decidability of Conversion for Type Theory in Type Theory.

It is not exactly the same setting, but, in the case of simply typed lambda calculus with coproducts, where eta-equality is also problematic, typing information can be quite useful for deciding syntactic eta-equality of terms. For instance, if you do not compare terms for eta-equality at their type, but if you first find a suitable isomorphic type and then cast the terms along the isomorphism, deciding term equality becomes easier (for details, see https://arxiv.org/abs/1502.04634v4 ). Perhaps a similar technique can be used in type theory.   

Best regards,

Danko