Hi, I'm Vojta

It's pronounced v-oi-ta. I'm a PhD student at Nantes Université, under supervision of Assia Mahboubi. I'm on the Gallinette team at Inria.

My academic interests are mostly (homotopy) type theory, proof assistants, formalized mathematics of all kinds, and category theory. Before getting into mathematics I got a bachelor's degree in informatics and software engineering, and I try to stretch my programming muscle as often as possible.

You can find me on Mastodon (@VojtechStep) and GitHub (@VojtechStep). I very infrequently contribute to a shared blog I run with my friends: actually.fyi.

Publications

Formalization of Homotopy Pushouts in Homotopy Type Theory

Repository, DSpace, PDF

Master's thesis at Charles University, defended in September 2024

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.

Lecture notes

Properties of type families over pushouts in Homotopy Type Theory

PDF

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.

Teaching

Please note that I no longer have access to the @fel.cvut.cz email address listed on some of the courses' pages.

Summer semester 2021/22

Winter semester 2021/22