Conferences and workshops
- Category Theory 2017 (Vancouver), as part of the Kan Extension Seminar II : When computational monads go clubbing
- Category Theory 2016 (Halifax) : Bifibrations of model categories
PhD thesis
Here is my PhD thesis
(And the defense Beamer slides are there.)
It was co-directed by Paul-André Melliès, computer scientist
at Université Paris Diderot, and Clemens Berger,
mathematician at Université de Nice. I defended on December
7th, 2018 in front of the jury composed with: Clemens Berger
(advisor), Hugo Herbelin (president), André Joyal
(reviewer), Peter LeFanu Lumsdaine (examiner), Paul-André
Melliès (advisor), Simona Paoli (examiner), Emily Riehl
(examiner) and Thomas Streicher (reviewer).
Very broadly, my thesis is a quest for categorical structures that can be used to interprete Martin-Löf's type theories and variants of such. One of the main goal is to reconcile Lawvere's view on categorical logic that he developed through hyperdoctrines and the likes with the type-as-fibrations philosophy initiated by Awodey and Warren and greatly advocated by Voevodsky in the description of its model of univalence in the category of simplicial sets.
In the process, with collaborators, we have designed a structure mixing Grothendieck bifibrations and model categories, and a theorem allowing for a generic construction of these structures. This result can be interpreted as a Grothendieck construction for pseudo functors valued in the 2-category of Quillen model structures, left Quillen functors between them and natural transformations. Hence we named Quillen bifibrations the new structures. The theorem about Quillen bifibrations can be understood without any reference to type theory and applies in particular to the construction of Reedy model structures. Homotopy categories of Quillen bifibrations have a peculiar behaviour and can be constructed in two successives localizations. What is odd is that both localization can be obtained by Quillen's homotopy quotient of a model category. The only subtility is that the intermediary model category might not have all pushouts or pullbacks: based on works by Jeff Egger, we show that Quillen's construction of the localization can still be carried out in that larger settings. In the study of thes homotopy category for Quillen bifibrations, it appears that there should be a variation on the structure of Grothendieck bifibration where (some of) the push functors are only defined up to homotopy.
The last part of the work I conducted in this thesis is an attempt to use the intuition developped through Quillen bifibrations in order to propose a treatment of Joyal's tribes in a fibrational setting. Tribes are minimalistic structures to interprete HoTT. They are reminiscent of Brown's categories of fibrant objects. Through the fibrational view, path objects in tribes can be understood as a result of "pushing" the terminal dependent type above a base type A over its diagonal. However this push is of the previously mentioned flavour: the universal property it satisfies is a homotopy universal property. Nevertheless this understanding of tribes makes a clear connection with Lawvere's view of the equality predicates in first-order logic (or even in extensional dpendent type theory): in a hyperdoctrine, the equality predicate for objects of sort A is the image (push) over the diagonal of the total predicate on A. In this work, we have designed a fibrational structure that generalizes tribes. To do so, we develop a framework for relative (orthogonal or weak) factorization systems: this is a 2-level version of the usual factorization systems, from which we recover the usual notion in degenerate cases.
Undergraduate research experience
Master of Research in CS
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 it 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). Get the mémoire (in french) and the oral presentation.
Master of Research in Mathematics
Here (in french) is my master thesis in mathematics. It 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.
Master of Research in Mathematics (1st year)
This (in french) is my first year master's thesis, about the use of Grothendieck toposes to prove the independance of the Continuum Hypothesis relatively to the theory ZFC. (There might be some imprecisions and wrong results too.)
Master of Research in CS (1st year)
The first year of the Master of Research at École Normale Supérieure requires a research intership that I have performed at Université du Québec à Montréal in team LaCIM under the direction of Srečko Brlek. The partially achived goal was to prove a conjecture about the conservation of the tiling property for a polyomino under some transformations. There is a report that I will put here someday... maybe... if I finally fix some issues in there. But you can have a look at the presentation (in english) of the result I did in a workshop.