Chapter 7 Notes

The notion of homotopy $n$-type in classical homotopy theory is quite old. It was Voevodsky who realized that the notion can be defined recursively in homotopy type theory, starting from contractibility.

The property “Axiom K” was so named by Thomas Streicher, as a property of identity types which comes after J, the latter being the traditional name for the eliminator of identity types. thm:hedberg is due to Hedberg [hedberg1998coherence]; [krausgeneralizations] contains more information and generalizations.

The notions of $n$-connected spaces and functions are also classical in homotopy theory, although as mentioned before, our indexing for connectedness of functions is off by one from the classical indexing. The importance of the resulting factorization system has been emphasized by recent work in higher topos theory by Rezk, Lurie, and others. In particular, the results of this chapter should be compared with [lurie:higher-topoi, §6.5.1]. In sec:freudenthal, the theory of $n$-connected maps will be crucial to our proof of the Freudenthal suspension theorem.

Modal operators in simple type theory have been studied extensively; see e.g. [modalTT]. In the setting of dependent type theory, [ab:bracket-types] treats the special case of propositional truncation ($(-1)$-truncation) as a modal operator. The development presented here greatly extends and generalizes this work, while drawing also on ideas from topos theory.

Generally, modal operators come in (at least) two flavors: those such as $\diamond$ (“possibly”) for which $A\Rightarrow \diamond A$, and those such as $\mathrm{\square }$ (“necessarily”) for which $\mathrm{\square }A\Rightarrow A$. When they are also idempotent (i.e. $\diamond A=\diamond \diamond A$ or $\mathrm{\square }A=\mathrm{\square }\mathrm{\square }A$), the former may be identified with reflective subcategories (or equivalently, idempotent monads), and the latter with coreflective subcategories (or idempotent comonads). However, in dependent type theory it is trickier to deal with the comonadic sort, since they are more rarely stable under pullback, and thus cannot be interpreted as operations on the universe $𝒰$. Sometimes there are ways around this (see e.g. [QGFTinCHoTT12]), but for simplicity, here we stick to the monadic sort.

On the computational side, monads (and hence modalities) are used to model computational effects in functional programming [Moggi89].A computation is said to be pure if its execution results in no side effects (such as printing a message to the screen, playing music, or sending data over the Internet). There exist “purely functional” programming languages, such as Haskell, in which it is technically only possible to write pure functions: side effects are represented by applying “monads” to output types. For instance, a function of type $\mathrm{𝖨𝗇𝗍}\to \mathrm{𝖨𝗇𝗍}$ is pure, while a function of type $\mathrm{𝖨𝗇𝗍}\to \mathrm{𝖨𝖮}(\mathrm{𝖨𝗇𝗍})$ may perform input and output along the way to computing its result; the operation $\mathrm{𝖨𝖮}$ is a monad. (This is the origin of our use of the adverb “purely” for the identity monad, since it corresponds computationally to pure functions with no side-effects.) The modalities we have considered in this chapter are all idempotent, whereas those used in functional programming rarely are, but the ideas are still closely related.

Title	Chapter 7 Notes