Sitemap

Page Not Found

CV-pdf

Presentation

Posts by Category

Posts by Collection

CV

Page Archive

Portfolio

Research work

Sitemap

Posts by Tags

Talk map

Talks and presentations

Teaching

Terms and Privacy Policy

Blog posts

Jupyter notebook markdown generator

A Coq Formalization of the Bochner integral

The Bochner integral is a generalization of the Lebesgue integral, for functions taking their values in a Banach space. Therefore, both its mathematical definition and its formalization in the Coq proof assistant are more challenging as we cannot rely on the properties of real numbers. Our contributions include an original formalization of simple functions, Bochner integrability defined by a dependent type, and the construction of the proof of the integrability of measurable functions under mild hypotheses (weak separability). Then, we define the Bochner integral and prove several theorems, including dominated convergence and the equivalence with an existing formalization of Lebesgue integral for nonnegative functions.

Arxiv

A poset-like approach to positive opetopes

We introduce in this paper a new formalisation of positive opetopes where faces are organised in a poset. Then we show that our definition is equivalent to that of positives opetopes as given by Marek Zawadowski.

Arxiv

Two equivalent descriptions of opetopes: in terms of zoom complexes and of partial orders

We introduce in this paper a definition of (non necessarily positive) opetopes where faces are organised in a poset. Then we show that this description is equivalent to that given in terms of constellations by Kock, Joyal, Batanin and Mascari.

Arxiv

A Type Theory for Presheaves Over a Reedy Category

We introduce a small type theory whose models are precisely the pesheaves over a given Reedy category C with a given system of coverings, satisfying a certain assumption of local finiteness and presentability. Our work is directly inspired from the Globular Type Theory of Benjamin, Finster and Mimram, and the Simplicial Type Theory of Riehl and Shulman

(∞, ω)-categories in Spatial Type Theory

Using the Spatial Type Theory introduced by M. Shulman, we present a type theory modeled by the ∞-topos of presheaves over the category Θ. In particular, we may carve out a type of weak (∞, ω)-categories by defining suitable Segal and completeness conditions. In many regards the approach we have taken follows the ideas introduced by E. Riehl and M. Shulman in their Simplicial Type Theory. In this paper we lay down those definitions and prove some properties, as a proof of concept for further development.

Towards a type theory for (∞, ω)-categories

Published: April 15, 2025

A presentation about CellTT, a directed homotopy type theory aimed to model weak (∞, ω)-categories. The talk was given at the occasion of the HoTT-UF Workshop 2025. This work is part of my thesis, under the supervision of Samuel Mimram.

DM d’Anniversaire 2019

, , 2019

Un sujet qui m’a été offert par mon frère à l’occasion de mes 19 ans, que j’ai typographié. Il y est question de completion d’espace métrique et de valeurs absolues sur le corps des rationnels. Il manque cependant la dernière partie sur le théorème d’Ostrowski.

Groupoïdification

, , 2023

Une promenade mathématique sous la forme d’un problème avec des questions. On s’y intéresse à la “Groupoïdification”: un processus qui consiste à remplacer des espaces vectoriels par des groupoïdes pour faire émerger davantage de structure (Plus généralement, ce genre de méthode s’inscrit dans le champ de recherche contemporain de la “catégorification”) Ce document est librement inspiré d’un billet de blog de John C. Baez, entre autres.