Starting August 2023, I will be a researcher at SINTEF Nord in Tromsø, Norway.
I received my Ph.D. from the University of Western Ontario under the supervision of Dan Christensen. My mathematical research interests relate to homotopy type theory, higher topos theory, and algebraic topology. I am also interested in formal verification, and I contribute to the Coq-HoTT library.
Previously, I studied at NTNU (MSc) and at EPFL (BSc).
4. Ext groups in Homotopy Type Theory [arXiv] joint with Dan Christensen. (submitted)
3. Central H-spaces and banded types [arXiv] joint with Ulrik Buchholtz, Dan Christensen, and Egbert Rijke. (submitted)
2. Formalising Yoneda Ext in Univalent Foundations [arXiv, doi] accepted to ITP 2023.
1. Univalent categories of modules [arXiv, doi] in Mathematical Structures in Computer Science.
Formalisation of the paper Central H-spaces and banded types (#1697, #1701). See the central-types repository.
Formalisation of Yoneda Ext (#1534, #1646, #1663, #1712, #1718, #1738). The long exact sequence is currently in a separate repository: Yoneda-Ext.Theory about object classifiers (#1524).
Characterisation of projective types (#1383).
Formalising Yoneda Ext in Univalent Foundations, ITP 2023, Białystok, Aug 2023.
Central H-spaces and banded types, HoTT 2023, CMU, May 2023.
Central H-spaces and their bands, Rochester Topology Seminar, Feb, 2023.
Central H-spaces and banded types (slides), HoTTEST, Nov 2022.
Internal Yoneda Ext groups (slides), Category Theory Octoberfest 2022, Oct 2022.
The moduli space of H-space structures, AMS Fall Eastern Sectional Meeting, Oct 2022.
The moduli space of multiplications on a space, UWO Math Graduate Seminar, Sep 2022.
The internal AB axioms (abstract), HoTT/UF 2022, Jul 2022.
Ext groups over a space, Young Topologists Meeting, Jul 2022.
Internal injectivity of modules in higher toposes (abstract), ASL 2022 North American Annual Meeting, Apr 2022.
Internally injective modules in higher toposes, Logic and higher structures, Feb 2022.
Ext groups in Homotopy Type Theory (abstract), HoTT/UF 2021, Jul 2021.
Higher Ext via profunctor tensor products, UWO Math Graduate Seminar, Oct 2020.
Programming with Category Theory, NTNU Geometry & Topology seminar, Feb 2019.
Elegant Parsing in Haskell, λ-Trondheim, Apr 2018.
Implementing a blockchain in Haskell, λ-Trondheim, Mar 2018.
You can contact me at jtaxers [at] uwo [dot] ca.