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