This thesis is based on five papers on the development of synthetic homotopy theory in homotopy type theory (HoTT), a relatively recent system of mathematics which extends Martin-Löf type theory with higher inductive types and univalence. The thesis is, in particular, concerned with the development of (co)homology theories and operations, but it also covers other (often related) cornerstone results from homotopy theory. Most results presented here have been computer formalised, i.e. digitally verified by a computer, in the verification software (or proof assistant) Cubical Agda.

Paper I presents a construction and computer formalisation of cohomology rings in HoTT. To this end, the associativity of cup products is proved – a seemingly easy problem which has turned out to be rather difficult in HoTT due to complicated coherences which arise when attempting a naïve proof. The paper also contains various computations of cohomology groups and rings, the Gysin sequence and a discussion of computational aspects of the computer implementation in Cubical Agda. The paper, in many ways, serves as an introduction to the remainder of the thesis.

Paper II presents a computer formalisation of Brunerie’s (2016) computation of the fourth homotopy group of the 3-sphere. In addition to this, we provide a vastly simplified version of Brunerie’s proof by introducing a new way of computing (both by hand and by normalisation in Cubical Agda) the so-called Brunerie number, i.e. the order of the homotopy group in question.

Paper III is devoted to solving another surprisingly difficult problem in HoTT, namely that of showing that the smash product is (1-coherent) symmetric monoidal. This is done by developing a heuristic for constructing homotopies over large iterated smash products. This heuristic is also expressed as a formal theorem which, in essence, presents iterated smash products as retracts of homotopically simpler spaces.

Paper IV presents work on cellular homology in HoTT. We develop basic theory of CW complexes and prove a constructive analogue of the cellular approximation theorem, as well as a special case of the CW-approximation theorem which states that two different notions of n-connectedness are equivalent. The cellular approximation theorem is then used to prove functoriality of cellular homology, and the special case of the CW-approximation theorem is used to prove the Hurewicz theorem. We also verify that our homology theory satisfies the Eilenberg–Steenrod axioms.

Paper V uses the cohomology theory from Paper I in order to construct the Steenrod squares, a set of cohomology operations for mod 2 cohomology. We use (and generalise) a definition of these operations due to Brunerie (2017), but go much further and prove their characterising properties, e.g. the Cartan formula and the Adem relations. This is done by reducing most problems to a ‘master theorem’ which is a simple-to-state but difficult-to-prove Fubini-like statement concerning so-called unordered joins. We use the squares to complete an alternative computation of the fourth homotopy group of the 3-sphere suggested in Paper II.