Hi, I am Felix Cherubini (birth name: Felix Wellen) and this is my research website.

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 synthetic algebraic geometry project I am currently working on, can be viewed here.

Events

• With Hugo Moeneclaey, I organized the fourth fourth workshop on synthetic algebraic geometry in Gothenburg, March 11-15, 2024.
• Talk at 37c3 on understanding HoTT via agda/programming. html notes.lagda.md
• With Marc Nieper-Wißkirchen, I organized the third synthetic algebraic geometry meeting October 2-6, 2023.
• I organized a second workshop on internal methods in algebraic geometry, April 17-20, 2023.
• I co-organized a spontaneous mini-workshop in Augsburg, in December 2022.
• I organized the workshop Geometry in Modal Homotopy Type Theory at CMU, March 11-15 2019.

Articles and Drafts

• A couple of drafts in which I am involved are in the synthetic algebraic geometry project

• A Foundation for Synthetic Algebraic Geometry, with T. Coquand and M. Hutzler, (accepted by MSCS), latest draft, arxiv, beginning formalization

• Synthetic G-jet-structures in Modal HoTT, (accepted by MSCS), latest draft, outdated arxiv, formalization,

• Modal Descent with Egbert Rijke, accepted 2020 for publication in MSCS, arxiv, (doi: 10.1017/S0960129520000201)

  Comment: There is a problem with theorem 3.10 (I don't know more so far).

  Comment: The name o-cover would have been better than o-étale.

• Formalizing Cartan Geometry in Modal Homotopy Type Theory, PhD-thesis, 2017, KIT library, formalization

  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.

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

Abstracts/Presented Ideas

• 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. Comment: There is now a draft on Cech-Cohomology which subsumes these ideas and works.

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

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

• 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

Notes

• I taught a course on HoTT at the University of Augsburg in the summer 2021. There is a german script.
• Short old note on a Mayer-Vietoris sequence for cohomology with dependent coefficients and similar things.
• notes on universal delta functors in HoTT, finally fixed.
• Fabian Endres' notes on an cubical-agda project concerned with groupification and monoid solving, which I supervised, in 2021.

Videos

I gave a hottest talk on synthetic algebraic geometry. The third workshop and fourth workshop on this topic have recordings.

Here is an overview of video recordings of talks about topics related to (differential) cohesive HoTT:

• 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

• I also gave a talk (on workshop website) at the workshop linked above.

Employment history

• In 2017 I finished my doctoral thesis in Karlsruhe, after working there for five years.
• Starting in fall 2017, I was a postdoc at Carnegie Mellon University (CMU) in Pittsburgh for 20 months.
• In 2019, I started an industry job as a software developer at the Softwareschneiderei GmbH in Karlsruhe, Germany.
• Two years later in 2021, I was at the University of Augsburg for half a year.
• Since fall 2021, I am at Chalmers/University of Gothenburg, Sweden.

Contact

You can use the address felix.cherubini[at]posteo.de to contact me.