Formalising a 1-categorical zigzag construction - A method for constructing the path spaces of pushouts formalised in the Lean proof assistant

Abstract

In homotopy type theory, which provides a synthetic foundation for mathematics by unifying type theory and homotopy theory, pushouts are fundamental for gluing spaces together. The path spaces of pushouts, which not only give insight to the truncation levels of a pushout, contain interesting structure. A construction of this space, the zigzag construction, has been formulated by Wärn and such a construction is well-suited for a formalisation effort in a proof assistant such as Lean to verify its correctness and provide further insight into its components. This thesis presents a 1-categorical zigzag construction based on Wärn’s formulation in (∞,1)-categories by constructing a number of 2-categorical pullbacks and showing a number of adjunctions between them. Some elementary category-theoretic results missing in Mathlib4, the main library for mathematics in Lean, are also formalised, notably the infrastructure around sequential colimits and special cases of 2-categorical limits and their properties.