Posts by Collection

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

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.