Academic website of Theofanis Chatzidiamantis-Christoforidis

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.