I am taking an introductory course on type theory. I find the following sentence in my handout:
''$a:A$ in $\Gamma$'' or ''$\Gamma\vdash a:A$'' is equivalent to the following judgment ''$a(x_1,...x_n):A(x_1,...,A_n)<x_1:A,...x_n:A_n(x_1,...,x_{n-1})>$'', where $\Gamma=<x_1:A,...x_n:A_n(x_1,...,x_{n-1})>$.
I understand that the latter hypothetical judgment simply makes explicit the assumptions contained in $\Gamma$. But I am wondering how we shall interpret $a(x_1,...x_n)$ in the latter notation. It is clear that $a$ in $a:A$ is a constant, but what about $a(x_1,...,x_n)$ if they are taken to be equivalent? How does $a(x_1,...,x_n)$ differ from a pure variable such as $x_{n+1}$?
Thanks!
Thinking of $\Gamma$ as a list of assumptions, the types and terms to the right of the $\vdash$ may vary depending on what assumptions are made. Thinking of $\Gamma$ as a list of variables, the types and terms of the right of the $\vdash$ may depend on the variables in $\Gamma$. So it's not that the '$a$' in $\Gamma \vdash a:A$ is constant—rather, it depends on the context.
For example, consider $$x : \mathbb{N} \vdash \langle 1, 2, \dots, x \rangle : \mathrm{List}_x(\mathbb{N})$$
Here $\mathrm{Lin}_x(\mathbb{N})$ refers to the type of lists of natural numbers of length $x:\mathbb{N}$.
Both the term $\langle 1, 2, \dots, x \rangle$ and the type $\mathrm{List}_x(\mathbb{N})$ depend on the variable $x:\mathbb{N}$; but that isn't to say that the term is the same thing as a pure variable of type $\mathrm{Lin}_x(\mathbb{N})$.