Hi, I am Felix Cherubini (birth name: Felix Wellen) and this is my research website.
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 synthetic algebraic geometry project I am currently working on, can be viewed here.
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.
Towards computing cohomology of dependent abelian groups extended abstracts for the Workshop "Homotopy Type Theory and Univalent Foundations" (workshop-page) online, 2022. draft with bugs, prerecorded talk.
Some simple higher rings extended abstracts for the Workshop "Homotopy Type Theory and Univalent Foundations" online, 2021
Comment: This approach to quotients of higher rings is not as general as I thought.
Modal Descent with Egbert Rijke, accepted 2020 for publication in MSCS, arxiv, (doi: 10.1017/S0960129520000201)
Cartan Geometry in Modal Homotopy Type Theory, preprint, 2018, arxiv, git
Cohesive Covering Theory extended abstracts for the Workshop "Homotopy Type Theory and Univalent Foundations" in Oxford 2018
Comment: There is a problem in the abstract: ∫₁ is not really known to be a modality like I defined it, but if you take the modality generated by the generators of 1-truncation and ∫, it will be the right thing.
Formalizing Cartan Geometry in Modal Homotopy Type Theory, PhD-thesis, 2017, KIT library, git
Comment: This is rather outdated, and you probably want to read the article two entries above… It does however contain more context and a comparison of a more classical, diagrammatic proof and a type theoretic proof of one of the main theorems - where the latter proof is simpler by orders of magnitude.
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
Here is an overview of video recordings of talks about my topics:
In March 2018 I gave an overview talk during the MURI-meeting (part 1 part 2).
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 general 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.cherubini[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