I am postdoc at the Universität Greifswald in Greifswald, Germany.
There I am a mathematician primarily interested in understanding the role of equalities in mathematics, otherwise known as homotopy theory.
I believe formalization of matheamtics via proof assistants can be an important step towards better understanding homotopy theory. As a result I have now commenced various formalization projects, including contributions to Coq UniMath and Rzk. In particular I am currently focused oon the following formalization projects:
- Double Categories: I am working on a formalization of double categories in Coq UniMath (jointly with Benedikt Ahrens, Paige North and Niels van der Weide).
- Formalization of ∞-Cosmoi: I have been contributing to the formalization of ∞-cosmoi due to Riehl and Verity via the proof assistant Lean.
- Simplicial Type Theory: I am contributing to the formalization of simplicial type theory, as defined by Riehl & Shulman.
More details my formalization work can be found in the repositories below!
More general information about me and my mathematical work can be found on my Academic Webpage.