How to define eta-equivalence for F-omega types? 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
The first approach is subsumed by the second, sort of (because the first approach is slightly broken).

One should never consider expressions with free variables without explicitly specifying a context in which they appear (this is a lesson one learns as soon as one wants to formalize $\forall$ and $\exists$ that are allowed to range over possibly empty types or sets).

In a single-sorted theory, equations without context $t_1 = t_2$ can always be equipped with a context $\Gamma \vdash t_1 = t_2 : S$ where $S$ is the single sort and $\Gamma = x_1 : S, \ldots, x_n : S$, with $x_i$ being the free variables in $t_1$ and $t_2$.

Leaving the context implicit like that is not quite right. For example, what if I want to write down an equation that involves $x_1$ and $x_2$ in a context which also mentions $x_3$? You might think that sort of thing is going to be useless, but it isn't, not if $x_3$ could come from an empty type.

Also, as soon as you think about categorical semantics you will see that it makes little sense to have bare equations without contexts.

So I would advise you to put your equations in contexts, and then use the shorter form as an abbreviation. One reference where everything is done explicitly in a context all the time is Bart Jacob's "Categorical Logic and Type Theory", Chapter 8 is about polymorphic type theory and might be of particular interest to you.