I am a mathematics PhD student at the University of Western Ontario,
supervised by Dan Christensen. I
like (homotopy) type theory, category theory, and mathematical
logic of all kinds.
I also like formalising mathematics in proof assistants; I mostly work in
Coq/Rocq (in particular, the
Coq-HoTT library), but I also like
Rzk and I should
learn to like Agda.
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.
I look like this.
Contact Information
News
Old News
-
[08.2026] I was a teaching assistant at
the ICERM workshop
Teaching Higher Category Theory with Computers.
-
[01-04.2026] I am supervising an
undergraduate student learning about
constructive mathematics and formalisation, as part of the
directed reading program at Western.
-
[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.
-
[02-04.2025] I supervised an undergraduate
student learning about model theory, as part of the directed
reading program at Western.
-
[11.2024-05.2025] I am formalising various
forms of the bar induction axiom and their implications in Coq
(in particular, the Coq-HoTT library). I'm also thinking about the
consequences of assuming such axioms from constructive mathematics in
homotopy type theory.
-
[07-08.2024] Together with Nima Rasekh, we
are wondering what we can prove about 2-Segal spaces synthetically, in
the setting of simplicial type theory.