in the first appendix of the HoTT book the type formers (or connectives) are defined to be primitive constants, e.g. $\sum_{x:A}B$ is defined as $c_{\sum}(A,\lambda x.B)$. I was wondering what the type of this primitive constant might be?
An intuitive guess would be $c_{\sum_{n}}:c_{\sum_{n+1}}(A,A\rightarrow \mathcal{U_n})\equiv \sum_{x:A}A\to \mathcal{U_n}$. This would lead to an infinite set of primitive constants that have to be introduced.
I wonder wether this is what the authers of the HoTT book intended or if there is another approach to formally introduce the type formers?
As this primitive constants do not reappear in the second appendix: is there no need to actually express the type formers as terms of homotopy type theory, or is formal correctness just sacrificed for a better reading experience?
Thanks in advance for any help. Cheers, Philipp
It doesn't have a type. In the first presentation, the terms are terms of the untyped lambda calculus. It is a Curry-style presentation where we have a collection of terms (i.e. the terms of the untyped lambda calculus), and we want to sort them into types. In this approach, it is quite common that a term may have multiple, unrelated types. The type, if any, of $c_\Sigma(A,\lambda x.B(x))$ depends on $A$ and $B$. If the term $A$ is sorted into type $\mathcal U_n$ and $B$ into $A\to\mathcal U_n$ then $c_\Sigma(A,\lambda x.B(x))$ will be sorted into type $\mathcal U_n$ for every $n$. If we talked about the term $\lambda A.\lambda B.c_\Sigma(A,\lambda x.B(x))$ there are multiple types this exact same term could be sorted into.
The second presentation is not an extension of the first. Instead, it is a Church-style presentation where the only terms that exist are well-typed terms. Note how values in the second presentation of the dependent function type $\prod_{x:A}B(x)$ are terms $\lambda (x:A).b$ while in the first presentation they are terms $\lambda x.b$. In a Church-style presentation, ill-typed terms are just meaningless just like syntactically malformed terms. Type constructors are analogous to logical connectives. They are not defined within the framework, instead they are part of the framework.
To be a bit more precise, in the Curry-style approach there is a set of terms (or better, terms-in-context) and a set of types and a relation relating the terms and the types. The terms can be defined on their own while the types (in a dependently typed calculus) are defined in terms of the terms and the typing relation relates these two pre-existing sets. (Actually, in dependently typed calculi types are terms and so there isn't usually a separate set of types.) In the Church-style approach, the set of terms, types, and the typing relation are all mutually recursively defined so there is no way of understanding the set of terms independently from the typing relation.
At any rate, the expression $\lambda(A:\mathcal U_n).\lambda(B:A\to\mathcal U_n).\sum_{x:A}B(x)$ is a function and thus a $\Pi$-type and would have type $\prod_{A:\mathcal U_n}[(A\to\mathcal U_n)\to\mathcal U_n]$. Or if we uncurry, we get a term of type $(\sum_{A:\mathcal U_n}(A\to\mathcal U_n))\to\mathcal U_n$. There would indeed effectively be a different term for each $n$, though some systems support universe polymorphism which would allow a single term for all $n$.