I am a mathematics PhD student at the University of Western Ontario, supervised by Dan Christensen. I like (homotopy) type theory, (higher) category theory, and mathematical logic of all kinds.

I am currently trying to figure out what type-theoretic versions of large cardinal axioms (large universe axioms?) would look like and understand their consequences in univalent category theory and algebra. I also like formalising mathematics in proof assistants, currently focused on doing constructive mathematics in Coq/Rocq (in particular, the Coq-HoTT library), and also having worked with Rzk and Lean.

I finished my master's at the University of Bonn in August 2024. I wrote my thesis on simplicial type theory, supervised by Nima Rasekh and Floris van Doorn.
Before that, I got my Bachelor's degree from the Aristotle University of Thessaloniki.

Contact Information

• Office MC275C. Department of Mathematics, University of Western Ontario
• email: tchatzid [at] uwo.ca
• github: thchatzidiamantis
• ORCID: 0009-0009-4619-182X

News

• [08.2026] I will be a teaching assistant at the ICERM workshop Teaching Higher Category Theory with Computers.
• [09-12.2025] I am supervising an undergraduate student learning about axiomatic set theory, as part of the directed reading program at Western.
• [09-12.2025] Together with Thomas Thorbjørnsen, we are organising a reading seminar on topos theory.