Jarl G. Taxerås Flaten

I am a fourth year Ph.D. student advised by Dan Christensen at the University of Western Ontario. My 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).

Publications & preprints

4. Ext groups in Homotopy Type Theory [arXiv], joint with Dan Christensen.

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], accepted to ITP 2023.

1. Univalent categories of modules [arXiv], to appear in Mathematical Structures in Computer Science.

Formalisation projects

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).

Upcoming & past talks

Formalising Yoneda Ext in Univalent Foundations, ITP 2023, Białystok, Jul 31 – Aug 4.

Central H-spaces and banded types, HoTT 2023, CMU, May 22–25.

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.

Mentoring & teaching

In Summer '22, I was a teaching assistant for the HoTTEST Summer School 2022.

Since Fall '21, I have been the lead organizer of the Directed Reading Program at Western. Before becoming an organizer, I mentored the following projects:

SOGS Running Club

I am the founder of the SOGS Running Club for graduate students at Western. Our weekly runs are currently on Tuesdays and Thursdays at 5:00pm. We meet by the entrance of the Western Recreation Center, and we usually do around 5-6km in under an hour. The runs are meant to be social, and runners of all experience levels are welcome! Send me an email (see below) and I'll invite you to our mailing list and group chat for updates and events.


You can contact me at jtaxers (at) uwo (dot) ca.