Master's thesis at Charles University
Abstract: Homotopy pushouts can be constructed as higher inductive types in the logical framework of Homotopy Type Theory, where one may engage syntactic methods to explore their properties, and formalize them in a proof assistant. This thesis focuses on the descent property, due to Rijke, which characterizes type families over pushouts; the flattening lemma, due to Brunerie, which characterizes the total spaces of such families; and the universal property of identity types of pushouts, due to Kraus and von Raumer. We also build elementary infrastructure for sequential colimits, following a paper of Sojakova, van Doorn, and Rijke. We then use the built machinery to provide a partial formalized proof of Wärn’s zigzag construction of identity types of pushouts as sequential colimits, leaving one coherence problem open. The thesis was simultaneously formalized in the proof assistant Agda and results contributed to the agda-unimath library.
May 23rd, 2024
Mathematics and Theoretical Computing seminar, FMF UL
Talk anouncement
Abstract: Homotopy Type Theory characterizes the identity type of universes via the univalence axiom, which allows us to construct non-trivial commuting diagrams involving the universe type. Those in turn provide a way to construct type families over higher inductive types.
The talk will explore the particular case of pushouts. We will characterize the data necessary to glue together a type family over a pushout (the descent property), and show that total spaces of such families are again pushouts (the flattening lemma). We conclude by using the built infrastructure to give an induction principle of identity types of pushouts.