Research

Books

• The book aimed at presenting basic group theory and connected subjects in univalent foundations directly. To some extent, group theory is mostly an abstraction invented to model the notion of symmetry. Our thesis at the basis of the book is that homotopy type theory has a built-in notion of symmetry that is more natural to use for such a modelisation. Namely, any element x of a type X comes equipped with the type (x=x) whose elemts can be understood as the synmmetries of x in X. Starting from this simple observation, we reconstruct group theory as the study of pointed 1-truncated connected types. The theory thus constructed has a very geometric feeling, that makes it very suitable for any application of group theory in algebraic topology.

Publications

• Working in univalent foundations, we investigate the symmetries of spheres, i.e., the types of the form 𝕊ⁿ=𝕊ⁿ. The case of the circle has a slick answer: the symmetries of the circle form two copies of the circle. For higher-dimensional spheres, the type of symmetries has again two connected components, namely the components of the maps of degree plus or minus one. Each of the two components has ℤ/2ℤ as fundamental group. For the latter result, we develop an EHP long exact sequence.
• Generalized Algebraic Data Types (GADTs) are a syntactic generalization of the usual algebraic data types (ADTs), such as lists, trees, etc. ADTs’ standard initial algebra semantics (IAS) in the category 𝑆𝑒𝑡 of sets justify critical syntactic constructs — such as recursion, pattern-matching, and fold — for programming with them. In this paper, we show that semantics for GADTs that specialize to the IAS for ADTs are necessarily unsatisfactory. First, we show that the functorial nature of such semantics for GADTs in 𝑆𝑒𝑡 introduces ghost elements, i.e., elements not writable in syntax. Next, we show how such ghost elements break parametricity. We observe that the situation for GADTs contrasts dramatically with that for ADTs, whose IAS coincides with the parametric model constructed via their Church encodings in System F. Our analysis reveals that the fundamental obstacle to giving a functorial IAS for GADTs is the inherently partial nature of their map functions. We show that this obstacle cannot be overcome by replacing 𝑆𝑒𝑡 with other categories that account for this partiality.
• It is well-known that GADTs do not admit standard map functions of the kind supported by ADTs and nested types. In addition, standard map functions are insufficient to distribute their data-changing argument functions over all of the structure present in elements of deep GADTs, even just deep ADTs or nested types. This paper develops an algorithm that characterizes those functions on a (deep) GADT’s type arguments that are mappable over its elements. The algorithm takes as input a term t whose type is an instance of a (deep) GADT 𝖦, and returns a set of constraints a function must satisfy to be mappable over t. This algorithm, and thus this paper, can in some sense be read as defining what it means for a function to be mappable over t: f is mappable over an element t of G precisely when it satisfies the constraints returned when our algorithm is run on t and 𝖦. This is significant: to our knowledge, there is no existing definition or other characterization of the intuitive notion of mappability for functions over GADTs.
• In this article, we develop a notion of Quillen bifibration whose purpose is to combine the two notions of Grothendieck bifibration and of Quillen model structure. In particular, given a bifibration p:E→B, we describe when a family of model structures on the fibers of p at A and on the basis category B combines into a model structure on the total category E, such that the functor p preserves cofibrations, fibrations and weak equivalences. Using this Grothendieck construction for model structures, we revisit the traditional definition of Reedy model structures, and possible generalizations, and exhibit their bifibrational nature.Oslo

Conferences and workshops

• Expanding the results from TYPES 2023, we show that GADTs cannot be interpreted as lax functors either on the category of sets and partial functions.
• GADTs cannot be interpreted as non-trivial functors on sets, even when we allow morphisms between sets to be partial functions.
• Presentation of the paper with the same name accepted for publication.
• Invited talk. Early communication about the results of the paper with the same name.
• Event cancelled because of COVID-19 outbreak.
• As part of the Kan Extension Seminar II.
• Presentation of On bifibrations of model categories at an early stage.

Preprints

• Working in univalent foundations, we investigate the symmetries of spheres, i.e., the types of the form 𝕊ⁿ=𝕊ⁿ. The case of the circle has a slick answer: the symmetries of the circle form two copies of the circle. For higher-dimensional spheres, the type of symmetries has again two connected components, namely the components of the maps of degree plus or minus one. Each of the two components has ℤ/2ℤ as fundamental group. For the latter result, we develop an EHP long exact sequence.
• The total category of a Quillen bifibration inherits a Quillen model structure whose homotopy category can be constructed in two successive homotopy quotients.
• This preprint is an attempt to reconcile Lawvere's definition of equality predicates in an hyperdoctrine and path objects interpreting MLTT's identity types in categories with enough homotopical structures (Quillen model category, Joyal's tribes, fibration categories, etc.)

Undergraduate research experience

• I graduated from École Normale Supérieure in Computer Science by doing a 5 month research internship under the supervision of Paul-André Melliès. During the internship, I designed a categorical framework, based on monads with arities, suitable to model memory allocation and deallocation in a quantum program (more generally in a program with linear ressource managment). Warning: both the thesis and the slides are in French.
• I obtained my Master degree in Pure Mathematics at Université Pierre et Marie Curie (Paris 6). My master thesis was directed by Georges Maltsiniotis and focused on the proof that Denis-Charles Cisinski gave of a conjecture made by Grothendieck in Pursuing Stacks: any basic localizer contains the weak homotopy equivalences. Warning: the thesis is in French.
• During the first year of my Master degree in Pure Mathematics at Université Pierre et Marie Curie (Paris 6), I write a memoir about the use of Grothendieck toposes to prove the independance of the Continuum Hypothesis relatively to the theory ZFC. This work was directed by Emmanuel Lepage. Warning: the thesis is in French.
• The first year of the Master of Research in CS at École Normale Supérieure requires a research intership, which I did at Université du Québec à Montréal in team LaCIM under the direction of Srečko Brlek. The goal was to prove a conjecture about the conservation of the tiling property for a polyomino under some transformations. The goal was partially achieved and the results collected in a memoir (not available, some issues need to be fixed). The slides available here were used during the workshop GTGeo 2013 to expose the results.
• I completed my bachelor degree in Computer Science at École Normale Supérieure, that requires a 2 to 3 mounth research internship. I worked at LORIA (Nancy) in team ADAGIo under the supervision of Damien Jamet and Eric Domenjoud. The internship concerned counting and generating local configurations of discretized plans. The internship included a coding part and a theoretical one. Warnign: the report is in French.