# Jarl G. Taxerås Flaten

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

### Publications & preprints

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

### Contact

You can contact me at *jtaxers* [at] *uwo* [dot] *ca*.