[Solved]: lambda calculus as a type theory

In the very next paragraph of that book (see HoTT, p. 2) they give an informal characterization of what qualifies a language system (or logic) as a type system, namely that: in it all terms are typed. By “Church’s type system” they’re referring to the simply typed lambda calculus (introduced in 1940).

In 1930s, in particular while preparing his negative solution to the decision problem, Church had introduced a system of untyped lambda calculus. This, of course, was not a type theory.

The 1940 system, however, is a type theory, because in it all terms are typed (see, for example (T&S), Section 1.2 for how exactly this is done). By “lambda-calculus as a type system” they’re referring to this second, simply typed version of lambda calculus. (T&S) Troelstra, A.S. & Schwichtenberg, H. Basic Proof Theory, 1996.