Research work

(∞, ω)-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.

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

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