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

Sammanfattning

In homotopy type theory, which provides a synthetic foundation for mathematics by unifying type theory and homotopytheory, pushouts are fundamental for gluing spaces together. The path spaces of pushouts, which not only give insightto 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 asLean to verify its correctness and provide further insight into its components. This thesis presents a 1-categorical zigzagconstruction based on Wärn’s formulation in (∞,1)-categories by constructing a number of 2-categorical pullbacks andshowing a number of adjunctions between them. Some elementary category-theoretic results missing in Mathlib4, the mainlibrary for mathematics in Lean, are also formalised, notably the infrastructure around sequential colimits and special casesof 2-categorical limits and their properties.