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.
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. published in Volume 9, Issue 2 of Higher Structues
We introduce a small type theory whose models are precisely the presheaves 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
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.
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. published in Volume 36, of Mathematical Structures in Computer Science doi
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.
A second presentation about CellTT, a directed homotopy type theory aimed to model weak (∞, ω)-categories. The talk was given at the occasion of a small workshop at IRIF, in Paris. This work is part of my thesis, under the supervision of Samuel Mimram.
A presentation of Bunched Affine Type Theory (BATT). This work is part of my thesis, under the supervision of Samuel Mimram.
abstract: The last two decades have seen the emergence of “homotopy” type theory (HoTT), in which intensional identity types can be interpreted as the space of paths connecting two points of a type. This new interpretation allows types in HoTT to be viewed as spaces up to homotopy, thereby providing a synthetic language well-suited to formalizing results specific to homotopy theory or to drawing parallels between mathematical logic and that field. More recently, we have seen the emergence of a variant of HoTT that allows us to work with a notion of “directed” spaces, up to homotopy — think of how directed graphs relate to undirected graphs. Within this setting, there is a concept of (directed) path types between two points of a given type, which in turn cannot yet be a directed space. We will explore an idea to remedy this shortcoming and enable the study of a higher version of directedness, where path types of directed types can themselves be directed (∞-groupoids). We will see along the way why it may be useful to consider an extension of the syntax where two kinds of context extensions coexist, akin to the Cartesian and linear pairing of contexts appearing in linear logic. The new pairing operation is being thought about as the Gray tensor product of categories, and its adjoints are to be interpreted as the categories of functors together with lax (resp. oplax) transformations. Such a system is known as “bunched logic” or “bunched type theory”. We will present a draft version of its rules and simple examples of its usefulness, for instance, in order to define the directed path type of a type.
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.
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.
This document is a follow-up to the assignment ‘The Fundamental Group’ and explores the fundamental group of roses (or bouquets of circles) through their universal covering.
