Some results in synthetic homotopy theory

Abstract

Synthetic homotopy theory is a relatively new approach to homotopy theory based on a variant of Martin-Löf type theory called homotopy type theory. A central theme of synthetic homotopy theory is the study of identity types, or path spaces, which describe the ways in which two elements of the same type can be equal. This thesis consists of two works in the field of synthetic homotopy theory which shed some light on the nature of identity types. The first and most significant consists of a precise and useful description of identity types of pushouts by what we call the zigzag construction. This can equivalently be seen as a description of the free ∞-groupoid on a graph of spaces. The zigzag construction notably has no exact classical counterpart and should be of interest also outside of type theory. In type theory, it provides a solution to a long-standing open problem in synthetic homotopy theory, namely the problem of showing that the suspension of a 0-type is 1-truncated. The second consists of an elementary treatment of stabilisation in spaces. This is the phenomenon that pointed types admit unique deloopings once they are sufficiently connected and truncated, and that pointed maps admit unique deloopings under similar conditions. This allows us to construct types with specified identity types. In particular we present a new description of Eilenberg–MacLane spaces.