What does $x : X$ mean? I've tried to learn type theory a few times, but the notation $x : X$ always trips me up. Does it mean:


*

*$x$ represents a fixed but arbitrary inhabitant of the type $X$?

*The variable $x$ is just "associated" to the type $X$, but not necessarily fixed. In particular, we can now write $\forall xPx$ as shorthand for $(\forall x : X)(Px),$ similarly we can write $\lambda x f x$ as shorthand for $(\lambda x : X)(f x)$ etc.

*Something else?


Thanks.
 A: When you formalize type theory it is probably easiest to work with expressions $C \vdash J$, where $C$ is a context, and $J$ is a judgement. A context is of the form $x_1 : A_1, \ldots, x_n : A_n$ where $x_i$ are free variables and $A_i$ are types. A judgement is either $t : A$ or $t \equiv s : A$ where $A$ is a type and $t$ and $s$ are terms. The terms $s$ and $t$ can contain free variables, but we only consider $C \vdash J$ when every free variable occurring in $J$ already appears in $C$.
When we see $x : A$ as part of a context it is an assumption, so we think of it as saying "for every $x$ of type $A$." However, exactly the same expression $x:A$ can also appear as the judgement $J$ (since each free variable is in particular a term). In this case we read it as saying "$x$ is an object of type $A$."
To give an easy example, we can prove in type theory $x:A, y:B \vdash (x, y) : A \times B$. This says that, given an object $x$ of type $A$ and an object $y$ of type $B$, the term $(x, y)$ is of type $A \times B$. We can also think of this as a function, that takes two inputs (one from $A$ and one from $B$) and produces an element of $A \times B$.
A: x such that the set X; ":" operator denotes "such that". It is basically its type.
$$a : b$$ and the description following the colon is actually the definition (b) of a.
