1. SYCO10 - Edinburgh (2022) slides
    Cubical type theory inside a presheaf topos.

Personal notes

  1. Notes on sheaf cohomology (2023) pdf
    Notes on the definition of sheaf cohomology in an arbitrary Grothendieck topos.

  2. Adjunctions, monads, and monadicity (2022) pdf
    This paper is a self-contained proof, in full details, and from (almost) scratch, of the monadicity theorem. We only assume the reader to be familiar with the basics of categories, functors, natural transformations, and the notion of coequalizer. We will give some examples and applications in further work.

  3. Category theory as a general tool for structures (2022) pdf
    An internship report in which I argue that category theory serves as a syntactic tool for studying very general types of structures. I give some foundational justifications with Husserl's phenomenology (edit 2023: I am thinking Deleuze now, they are pure movements), and I continue with the study of social interactions seen as Kan extensions. In French.

  4. On the Yoneda Lemma (2022) pdf
    Small paper where I try to give some intuition about the notion of presheaf, prove the Yoneda Lemma and the density formula.

Academic Papers

  1. Cubical Type Theory Inside a Presheaf Topos (2022) pdf
    Summer '22 internship, for my Master's thesis. I worked on the use of Kripke-Joyal semantics to prove that the presheaves over the category of free de Morgan algebras are a model of cubical type theory. Here are the slides for my defense. I was supervised by Pierre-Louis Curien.

  2. Category theory in Coq (2022) github
    Final project of the LMFI's course 'Functional programming and formal proofs in Coq' where a student and I (re)implemented basics of category theory in Coq.

  3. Loops of Csörgő Type and the AIM Conjecture (2021) pdf
    Summer '21 internship.