Hi, I am Felix Wellen and this is the my research website. I am currently working as a postdoc at Carnegie Mellon University (CMU) in Pittsburgh.

## What my research is about

I am interested in application of Homotopy Type Theory (HoTT) to Differential and Algebraic Geometry and, more generally, I want to know how well HoTT can help to make current research in pure mathematics more understandable. The approach I am using is based on Urs Schreiber's differential cohesion.

In early 2018, I wrote an essay describing my thesis for the German competition "Klartext!". It didn't win and it is in German, you can view it here.

## Events

I organized a workshop called "Geometry in Modal Homotopy Type Theory" which took place March 11-15 at CMU.

## Written work

There is a draft of an article on cartan geometry in modal HoTT. This contains a lot of the content of my thesis. There are some improvemts and new theorems. Here is my thesis Formalizing Cartan Geometry in Modal Homotopy Type Theory. And here is the git repo for the thesis, which also contains more recent stuff. Here is the nLab page of the project. Here is the complete list: There are two extended abstracts for the Workshop "Homotopy Type Theory and Univalent Foundations" in Oxford:

- Cartan Geometry in Modal Homotopy Type Theory, article in peer review, 2018, arxiv, git
- Cohesive Covering Theory extended abstracts for the Workshop "Homotopy Type Theory and Univalent Foundations" in Oxford 2018
- Formalizing Cartan Geometry in Modal Homotopy Type Theory, PhD-thesis, 2017, KIT library, git
- Differential Cohesive Type Theory with Jacob A. Gross, Daniel R. Licata, Max S. New, Jennifer Paykin, Mitchell Riley, Michael Shulman. extended abstracts for the Workshop "Homotopy Type Theory and Univalent Foundations" in Oxford 2017

## Videos

Together with Dan Licata, I gave a tutorial at the workshop on Homotopy Type Theory during the Hausdorff Trimester on Types, Sets and Constructions. It was about Modal Homotopy Type Theory and there are recordings on Youtube listed below. What I write on the blackboard is even less readable than usual though.

This one might be the best place to start, if you want to understand the genral direction of what I am interested in.

This one focuses on the cartan geometry from my thesis.

Those were tutorials 2 and 6, here is the complete list:

Tutorial 1 Dan Licata: A Fibrational Framework for Modal Simple Type Theories

Tutorial 2 Felix Wellen: The Shape Modality in Real cohesive HoTT and Covering Spaces

Tutorial 3 Dan Licata: Discrete and Codiscrete Modalities in Cohesive HoTT

Tutorial 4 Felix Wellen: Discrete and Codiscrete Modalities in Cohesive HoTT, II

Tutorial 5 Dan Licata: A Fibrational Framework for Modal Dependent Type Theories

Tutorial 6 Felix Wellen: Differential Cohesive HoTT

You can use the address felix.wellen[at]posteo.de to contact me. There is also a pgp-key for this address with fingerprint 63E6 E9E2 D88A 267B 7A44 5A34 62D3 070A CDC1 004E