It's pronounced v-oi-ta. I'm a PhD student at Nantes Université, under supervision of Assia Mahboubi and Cyril Cohen. 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.
Until April 2026 I was a contributor and maintainer of the agda-unimath library, a library of HoTT-based mathematics formalized in Agda.
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.
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.
May 6th, 2026 at TYPES
Abstract Parametricity in dependent type theory is presently used to power automation frameworks for data refinement and proof transfer, to derive theorems for free. In this talk, we leverage a parametricity translation à la Trocq to automatically derive definitions, specifically the types of morphisms of structures. We show how our framework accommodates structures outside of the most frequently considered fragment (GATs), such as posets with order reflecting maps or topological spaces with continuous maps.
Joint work with Assia Mahboubi and Cyril Cohen.
April 10th, 2026 at the Student PL Meetup
January 17th, 2026 at RocqPL
Abstract: In dependent type theory, parametricity is often written as a function structurally recursive on the abstract syntax tree of terms. We identify a shortcoming of the functional presentations and offer an alternative in the style of a sequent calculus, and further illustrate how it can be implemented as a logic program using the Rocq-ELPI metaprogramming framework. We also offer two extensions of binary parametricity to cover features of Rocq, namely translating fixpoint operators and record types.
Joint work with Cyril Cohen.
July 31st, 2025 at the Student PL Meetup
June 3rd, 2025 at ‹Programming›
Abstract:
Parametricity is a property of various type theories which enables
constructing relational interpretations. In dependent type theories,
this interpretation may be implemented as a metaprogram, translating
well-typed terms in the source language into relatedness proofs, in the
same language. E.g. using binary parametricity, two types A, B :
□ are related by the translation ⟦□⟧ A B := A → B →
□; two functions f : A → B, g : A’ → B’ are related
by the translation ⟦A → B⟧ f g if two related
inputs a, a’ are taken to two related outputs f a, g
a’, etc. This translation has practical applications, as it
generates
theorems for free
.
Multiple implementations of parametricity are available for the Rocq proof assistant, but so far records types have been treated as second-class citizens — the record is first translated into its representing inductive, which is then translated using parametricity. The resulting inductive, however, is an indexed inductive type, so it isn’t a direct representation of any record type. I will present the necessary changes to the rocq-elpi implementation of parametricity to support first-class record types.
April 22nd, 2025
Invited lecture, Faculty of Electrical Engineering, CTU in Prague
April 15th, 2025 at the Workshop on Homotopy Type Theory / Univalent Foundations
What the abstract doesn't mention is that the formalization was successfully completed on March 22nd. Consult the associated PR#1370.
Abstract: This talk presents the current state of my formalization of the zigzag construction due to Wärn. In 2023, Wärn published a note on his construction of identity types of pushouts from sequential colimits connected by a ”zigzag”. This explicit construction helps concretely understand higher path spaces of pushouts. It was carried out in a general enough higher categorical setting that it is expected to be definable and provable correct in a proof assistant implementing Homotopy Type Theory.
However, no complete formalization has been published to date. I take this opportunity to report on my attempt, which began in my master’s thesis. The formalization builds on and extends the agda-unimath library of univalent mathematics, which uses the Agda proof assistant with no cubical features. The intention of upstreaming the code motivates the development of reusable infrastructure for synthetic homotopy theory, as demonstrated by changes already submitted to the library.
May 23rd, 2024 at the Mathematics and Theoretical Computing seminar, FMF UL
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.
April 24th, 2024 at the #lang-talk meetup
Abstract: A brief introduction to dependent type theory, aimed at programmers who have heard about propositional logic, first order logic, and the lambda calculus.
Please note that I no longer have access to the @fel.cvut.cz email address listed on some of the courses' pages.