I am postdoc at the Max-Planck-Institut für Mathematik in Bonn, 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).
- 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.