Andrej’s answer gives an excellent list of resources. But I think it’s also worth saying a little upfront to ward off common misunderstandings. HoTT is a *foundational system* — analogous to ZFC set theory — and the way in which the basic vocabulary of foundational systems is “defined” is a bit different from how most mathematical objects are defined. And for newcomers to type theory, especially experienced mathematicians, this is a frequent source of misaligned expectations.

Whenever you’re setting up some logical formal system, you are typically “defining” things in several different senses:

you’re defining the formal system itself — its syntax, its rules of inference, its axioms…

you’re introducing terminology to talk about the basic notions of the formal system

as you work *within* the formal system, you’re then defining further objects within it.

With ZFC, for instance:

This is the sense in which you define what “first-order logic” and “ZFC” formally are, for studying them from the outside as a logician.

This is the sense in which you define *set*, *implies*, *for all*, and so on. You don’t define “a *set* is a such-and-such satisfying the so-condition”. We just introduce *set* as a word for the primitive objects that the ZFC axioms axiomatise. Similarly, *implies* is just a certain primitive symbol of our language, and first-order logic gives us rules for reasoning with it.

This is the sense in which you define *power sets*, the *rank* of sets, and generally, definitions made while doing mathematics within ZFC.

So (1) and (3) are definitions in the usual mathematical sense, but happening at two different levels — *external* to the formal system under consideration, or *internal* to it. Meanwhile, (2) is a bit more different: you are “defining” things by taking them as primitive notions and axiomatising them.

I say all this because **most of the things you mention in your question are “defined” in HoTT in sense (2) — so you will not find definitions of them in the sense you may expect! They are “defined” in the same way that ***sets* are defined by ZFC. Following through the senses above, for HoTT:

This is the sense in which you define what “HoTT” is, as a formal system from the outside. (HoTT and other type theories don’t have the same kind of separation between the “logical language” and the “theory in it” that you have with e.g. FOL+ZFC.)

This is the sense in which you define *type*, *term*, *for all*, and so on: They’re the words we use for the various primitive objects and symbols of the formal system; and the formal system gives us rules for reasoning with them.

This is the sense in which you define *contractible*, *eqivalence*, *univalent*, and so on, when developing mathematics within type theory.