There are (at least) two styles for defining a (declarative) equivalence judgement for a typed lambda calculus:
- via a plain relation $t_1 = t_2$,
- via an indexed relation $\Gamma \vdash t_1 = t_2 : T$.
Barendregt [1] e.g. uses the simpler former style, while other sources often seem to be preferring the latter.
I have only seen the first style being used for the case of simple beta equivalence (as in Barendregt). Is it possible to use this style even in the presence of an eta-rule, esp considering that eta-expansion does not necessarily preserve well-formedness?
More specifically, I'm interested in the (simple?) case of eta-equivalence for F-omega types. Any pointers are welcome.
[1] H. Barendregt, Lambda Calculi With Types. In: Handbook of Logic in Computer Science, Vol 2. Oxford University Press 1992