HoTT on wellformedness of contexts

Stream: maths

[Matt Yan]

949D72DF-14AA-4C70-8434-7D44A2818AA0.jpg

[Matt Yan]

Screenshot is from the HoTT book, Appendix, Peliminaries. there are two things I don't understand...essentially the entire paragraph.
First, each Ai needs to be one of A1, A2 ...A_i-1? apply this inductively, doesn't that mean all the types from A 1 to An has to be identical?

[Matt Yan]

and second, what does it mean by "Ai contains only the variables x1,...,x_i-1"?

[Matt Yan]

does the last sentence "and that a and A contain only the variable x_1,...,x_n" mean "and that A contains only the variable x_1,...x_n, a" instead?

[Floris van Doorn]

First question: I understand the ambiguity; it doesn't mean that $A_i$ is one of the previous types, but that it is a well-formed type with respect to the context $x_1:A_1, x_2:A_2,\ldots,x_{i-1}:A_{i-1}$. So it means
$x_1:A_1, x_2:A_2,\ldots,x_{i-1}:A_{i-1}\vdash A_i:\mathcal{U}$ or $x_1:A_1, x_2:A_2,\ldots,x_{i-1}:A_{i-1}\vdash A_i\textrm{ type}$ (depending on the notation used).

[Floris van Doorn]

Second question: Every term and type can be written as a string of letters and symbols. Some of these represent variables, and it just means that the only free variables that can occur in $A_i$ must be in the set $\{x_1,\ldots,x_{i-1}\}$.

[Floris van Doorn]

I think they are imprecise omitting the word "free". Variables bound by $\lambda$ are allowed to be outside this set (or maybe they mention this elsewhere).

[Floris van Doorn]

Last question: No, they mean what they write. Note that $a$ is in general not a variable, but could be a term, like $\lambda f. f(x_1)$.

[Matt Yan]

@Floris van Doorn Thanks! you reminded me that the entire thing is meta-theoretic about symbols and I was thinking internally all the time.

[Matt Yan]

Actually the fist half is internal yet the second half is meta..anyways thanks a lot