## Xuanrui Qi

I am Xuanrui Qi (亓璇睿), a third-year PhD student at the Graduate School of Mathematics, Nagoya University advised by Professors Jacques Garrigue and Lars Hesselholt. Broadly speaking, my research interests are in type theory and topos theory, and particularly in connection to geometry and topology.

I hold two master's degrees: a MS in mathematics from Nagoya University (2021), and a MS in computer science from Tufts University in the United States (2019). I did my undegraduate studies at, and received my bachelor's degree in computer science and international relations from Tufts University in 2018.

I am fortunate to be supported financially by the Japan Science and Technology Agency (JST)'s SPRING program, through participation in the Tokai National Higher Education & Research System (THERS) "Make New Standards Program for Next Generation Researchers".

You can find a copy of my CV here.

### Contact Information

- Email: xuanrui@nagoya-u.jp, me@xuanruiqi.com (if you are an recruiter from industry)
- Mailing address: Graduate School of Mathematics, Nagoya University, Furo-cho, Chikusa-ku, Nagoya, Aichi, Japan 464-8602
- GitHub: @xuanruiqi
- ORCID: 0000-0002-2032-1552
- PGP public key: 87F900026E06FBC8

### Research

My research interests could be broadly categorized as type theory and topos theory. Currently, I am mostly interested in homotopy type theory (HoTT) and ∞-topos theory, and in particular the use of modal HoTT as a language for developing geometry and topology, most importantly algebraic geometry, internally to an ∞-topos.

I am also interested in various related areas:

- abstract approaches to non-commutative geometry;
- categorical foundations of quantum information;
- categorical logic in general;
- the design and implementation of proof assistants;
- formalized mathematics;
- applied algebraic topology and in particular persistence theory.

Previously I also did research in various areas in theoretical computer science, such as design and implementation of type systems. I was involved in the formalization of OCaml's type system.

### Trivia

I have an Erdős number of at most 5.