Formalisation
In Coq/Rocq
Compact and Searchable Types [code].
Following work of Martin Escardó and Ayberk Tosun in Agda.
Bar Induction [code].
Bar induction axioms commonly appear in constructive mathematics. Here we define them in homotopy type theory in terms of list types.
Uniform Structures and Sequences [code].
Inspired by uniform spaces in topology, we can use these structures to talk about continuity in the constructive sense, e.g. about functions of type (\(\mathbb{N}\) -> X) -> (\(\mathbb{N}\) -> Y).
In Rzk
2-Segal Types [code].
Dependent Composition [code].
Master's thesis
Formalizing Higher Categories [pdf].
We formalise parts of Riehl and Shulman's theory of synthetic \(\infty\)-categories (i.e., simplicial type
theory) in the Rzk proof assistant. We also propose a definition of 2-Segal spaces in simplicial type theory.