Research

Books

Publications

Conferences and workshops

Preprints

PhD thesis

Jointly directed by Paul-André Melliès (Université de Paris) and Clemens Berger (Université de Nice — Sophia Antipolis).

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

Broadly speaking, 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, I 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. For that reason, this new notion is named Quillen bifibration. 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 more general setting. In the study of the 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 dependent 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