Have I written this statement correctly?

Question

I have written the following intentionally false statement:
f(x:t) ⊢ y:u ∴ u = t

This is intended to express that:
x of type t causes y of type u, therefore u is equal to t

Have I correctly expressed this statement?

Answer 1

Generally a typing statement has the form $$\frac{\Gamma\vdash \mathcal J}{\Delta\vdash \mathcal J'}$$ where $\Gamma,\Delta$ are contexts, that is sequences of typing judgements $x_1:\tau_1,\ldots,x_n:\tau_n$, and $\mathcal J,\mathcal J'$ are judgements, which could mean several different things depending on the type theory.

The above can be interpreted to mean "If $\mathcal J$ holds in context $\Gamma$, then $\mathcal J'$ holds in context $\Delta$".

In particular you can have a typing judgement $\mathcal J$ relating a term $t$ and a type $\sigma$, which you write like $t : \sigma$. You can also have an equality judgement relating two terms $s,t$ of a type $\sigma$, for which you could write $s = t : \sigma$. You might also have an equality judgement relating two types $\sigma,\tau$, which you might write $\sigma = \tau$.

In particular for your example, the left hand side $f(x:t)$ does not make sense as a context. However it would be reasonable to write something like

$$\frac{x_1:\tau_1,\ldots,x_n:\tau_n\vdash f(x_1,\ldots,x_n) : \sigma}{x_1:\tau_1,\ldots,x_n:\tau_n\vdash \sigma = \tau_1}$$

And if you are dealing with simply typed lambda calculus, the types $\sigma$ and $\tau_1$ do not depend on variables $x_1,\ldots,x_n$, so it would be okay to write the conclusion in an empty context like so:

$$\frac{x_1:\tau_1,\ldots,x_n:\tau_n\vdash f(x_1,\ldots,x_n) : \sigma}{\vdash \sigma = \tau_1}.$$