Formal definition of homotopy type theory

Here are some resources:

1. The appendix of the homotopy type theory book gives two formal presentations of homotopy type theory.
2. Martín Escardó wrote lecture notes Introduction to Univalent Foundations of Mathematics with Agda which are at the same time written as traditional mathematics and formalized in Agda (so as formal as it gets).
3. Designed for teaching purposes is Egbert Rijke's formalization HoTT-intro which accompanies his upcoming textbook on homotopy type theory.
4. The HoTT library is a formalization of homotopy type theory in Coq. Start reading in the order of files imported in HoTT.v.
5. The HoTT-Agda library is quite similar to the HoTT library, except formalized in Agda.
6. The UniMath library is another formalization of univalent mathematics in Coq.

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:

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

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

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

With ZFC, for instance:

1. 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.

2. 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.

3. 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:

1. 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.)

2. 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.

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