Your favourite piece of mathematics!
You can try and take your favourite piece of mathematics and develop it inside HoTT. This may be elementary group theory, some linear algebra, possibly something in analysis, or anything else. It will be a worthwhile exercise to try and see how much of it can be developed in HoTT as a constructivist foundation without assuming the law of excluded middle, and how one can find constructive versions of the standard theorems with non-constructive proofs. If your favorite piece of mathematics is category theory, set theory, or the real numbers, you can work with the corresponding chapter in the book.
Necessary background: if your particular piece of mathematics comprises quotients—like quotient groups or quotient vector spaces—some knowledge and understanding of higher inductive types may be necessary; see Chapter 6 in the book.
Heterogeneous equality
The usual identity types can only be formed between elements of the same type. However, another kind of identity types exist which permit the comparison of elements of different types; this is heterogeneous equality. You can study heterogeneous equality and how it relates to ordinary equality, as in the above link. This can be formalized in Coq (but doesn't have to).
Necessary background: nothing beyond the first half of the course.
The Hopf fibration
The Hopf fibration is a particularly fascinating topological object. You can try to understand how the Hopf fibration arises from a type family over the circle, how it gives rise to the homotopy group π3(S2) = ℤ, and possibly higher-dimensional versions of it.
Necessary background: nothing beyond the course.
The homotopical structure of the universe
The proof of Theorem 4.1.3 uses the universe to construct a type X behaving like an Eilenberg–Mac Lane space for the group of order 2. Which other spaces can be "carved" out of the universe like this? Can one obtain the circle and the spheres using similar constructions? Maybe even every finite CW complex?
Necessary background: nothing beyond the course plus Chapter 6 of the book.
Cohesive homotopy type theory
Cohesion consists of additional structure on types, e.g. differentiable structure, which allow one to do geometry on the level of types (as opposed to just topology, as in bare HoTT). You can study cohesive HoTT, possibly together with its implementation in Coq, and write an exposition of what you have learned and possibly coded.
Necessary background: some familiarity with category theory, in particular with adjoint functors, will help.
Girard's paradox
Girard's paradox is a type-theoretic variant of Russell's paradox which states that having only one universe as the type of all types is inconsistent. Try to explain Girard's paradox in your own words. How does the construction work? What is its intuitive meaning and how is it related to Russell's paradox (if at all)?
Necessary background: reading the literature requires some familiarity with the formal definition of type systems.
Semantics
This concerns models of homotopy type theory in conventional foundations. Finding such models is important since it shows that HoTT is at least as consistent as conventional foundations are. Also, HoTT is conjectured to be the internal language of (∞,1)-topoi, which comprises the hypothesis that every (∞,1)-topos models HoTT. The main problem here lies in proving that the univalence axiom holds. The first model to be found interprets every type as a simplicial set. You can try to understand the proof showing that the univalence axiom holds and formulate it in your own words.
Necessary background: this requires a substantial amount of background in category theory and on simplicial sets.