Context in context of Type Theory

Question

I am reading a book on homotopy type theory or let me better say 'the' book of HoTT. On page 416, the author intruduces a judgment that includes the ctx (context) formalism. The judgment

$$(x_1 : A_1, x_2 : A_2, ... , x_n : A_n) \text{ ctx }$$

expresses that each $A_i$ is a type in the context $x_1 : A_1, x_2 : A_2, ... , x_{i-1} : A_{i-1}$. The next statement I not understand:

In particular, therefore, if $\Gamma \vdash a : A $ and $\Gamma \text{ ctx } $, then we know that each $A_i$ contains only the variables $x_1, ... , x_{i-1}$, and that $a$ and $A$ contain only the variables $x_1, ... , x_n $.

As far I not understand this conclusion. By definition the judgement $\Gamma \vdash a : A $ means just that $a: A$ in context of $\Gamma $. Literally: $a$ has type $A$ under the assumptions listed in $\Gamma$.

The judgment $\Gamma \text{ ctx } $ says literally that the context $\Gamma$ is well-formed. As far as I understand it correctly, formally this is by definition above the statement that if $\Gamma = (x_1 : A_1, x_2 : A_2, ... , x_n : A_n)$ then that just means recursively that $A_i$ is a type in the context $x_1 : A_1, x_2 : A_2, ... , x_{i-1} : A_{i-1}$. Can it be token as general 'definition' of $\Gamma \text{ ctx } $, am I right?

But then, why from $\Gamma \vdash a : A $ and $\Gamma \text{ ctx } $ we conclude that $A_i$ contains only the variables $x_1, ... , x_{i-1}$ and that $a$ and $A$ contain only the variables $x_1, ... , x_n $? This 'conclusion' isn't clear for me.

Answer 1

The sentence you are quoting is part of an introduction, meant to give you some intuition behind the formalism of the theory. It does not pretend to give you the meta-theoretical proof that you are looking for: it says "then we know ...", not "this is a proof that ...".

In other words, the formal rules of the theory are designed so that in a context $\Gamma$:

• the type $A_i$ may refer only the the variables $x_0, ..., x_{i-1}$
• the terms $a$ and $A$ may refer only to the variables $x_0, ..., x_n$

To have a proof of it, you need to check -all- formal rules of the theory, verify that the rule "Vble" in A.2.2 is the only one to introduce fresh variables, and does it only in a context where this variable is already defined by its type.