In homotopy type theory, few constructions have proved as troublesome as the smash product. While its definition is just as direct as in classical mathematics, one quickly realises that in order to define and reason about functions over iterations of it, one has to verify an exponentially growing number of coherences. This has led to crucial results concerning smash products remaining open. One particularly important such result is the fact that the smash product forms a (1-coherent) symmetric monoidal product on the universe of pointed types. This fact was used, without a complete proof, by, for example, Brunerie ((2016) PhD thesis, Université Nice Sophia Antipolis) to construct the cup product on integral cohomology and is, more generally, a fundamental result in traditional algebraic topology. In this paper, we salvage the situation by introducing a simple informal heuristic for reasoning about functions defined over iterated smash products. We then use the heuristic to verify, for example, the hexagon and pentagon identities, thereby obtaining a proof of symmetric monoidality. We also provide a formal statement of the heuristic in terms of an induction principle concerning the construction of homotopies of functions defined over iterated smash products. The key results presented here have been formalised in the proof assistant Cubical Agda.

Working in homotopy type theory, we introduce the notion of n-exactness for a short sequence $F\to E\to B$ of pointed types and show that any fiber sequence $F\hookrightarrow E \twoheadrightarrow B$ of arbitrary types induces a short sequence

that is n-exact at $\| E\|_{n-1}$. We explain how the indexing makes sense when interpreted in terms of n-groups, and we compare our definition to the existing definitions of an exact sequence of n-groups for $n=1,2$. As the main application, we obtain the long n-exact sequence of homotopy n-groups of a fiber sequence.

Cubical methods have played an important role in the development of Homotopy Type Theory and Univalent Foundations (HoTT/UF) in recent years. The original motivation behind these developments was to give constructive meaning to Voevodsky’s univalence axiom, but they have since then led to a range of new results. Among the achievements of these methods is the design of new type theories and proof assistants with native support for notions from HoTT/UF, syntactic and semantic consistency results for HoTT/UF, as well as a variety of independence results and establishing that the univalence axiom does not increase the proof theoretic strength of type theory. This paper is based on lecture notes that were written for the 2019 Homotopy Type Theory Summer School at Carnegie Mellon University. The goal of these lectures was to give an introduction to cubical methods and provide sufficient background in order to make the current research in this very active area of HoTT/UF more accessible to newcomers. The focus of these notes is hence on both the syntactic and semantic aspects of these methods, in particular on cubical type theory and the various cubical set categories that give meaning to these theories.