Research
Research
Univalent mathematics, the semantics of data types, and homotopical algebra. Below: publications, my thesis, talks, notes, and the student research that came before.
Overview
Three threads run through my work. They meet in type theory, where homotopy theory, logic and programming languages share one language.
Univalent mathematics
In univalent foundations, every element \(x\) of a type comes with the type \(x = x\) of its symmetries. With coauthors, I use this to rebuild group theory in the book Symmetry, and to compute the symmetries of spheres.
Data types
Generalized algebraic data types (GADTs) are everyday tools of functional programming, but their semantics is subtle. With Patricia Johann, I study which functions can be mapped over them, why they are not functors, and what parametricity means for them.
Homotopical algebra and logic
My thesis combined Grothendieck bifibrations with Quillen model structures into Quillen bifibrations, and used them to read the identity types of dependent type theory as Lawvere's equality predicates.
The first result of the paper on spheres fits in a picture.
Publications
Book
-
draft
Symmetry
Marc Bezem, Ulrik Buchholtz, Pierre Cagne, Bjørn Ian Dundas, Daniel R. Grayson
Book in preparation.
About the book
The book presents basic group theory and related subjects directly in univalent foundations. Group theory is, to a large extent, an abstraction invented to model the notion of symmetry. The thesis at the basis of the book is that homotopy type theory has a built-in notion of symmetry that is more natural for this purpose: any element \(x\) of a type \(X\) comes with the type \(x = x\), whose elements can be understood as the symmetries of \(x\) in \(X\). Starting from this observation, we reconstruct group theory as the study of pointed, connected, 1-truncated types. The resulting theory has a very geometric feel, which makes it well suited to applications of group theory in algebraic topology.
Articles
-
2024
On symmetries of spheres in univalent foundations
Pierre Cagne, Ulrik Buchholtz, Nicolai Kraus, Marc Bezem
Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS '24), pp. 1–14.
Abstract
Working in univalent foundations, we investigate the symmetries of spheres, i.e., the types of the form \(\mathbb S^n = \mathbb S^n\). 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 \(\mathbb Z/2\mathbb Z\) as fundamental group. For the latter result, we develop an EHP long exact sequence.
BibTeX
@inproceedings{CagneBuchholtzKrausBezem2024, author = {Cagne, Pierre and Buchholtz, Ulrik and Kraus, Nicolai and Bezem, Marc}, title = {On Symmetries of Spheres in Univalent Foundations}, booktitle = {Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science}, series = {LICS '24}, pages = {1--14}, publisher = {ACM}, year = {2024}, doi = {10.1145/3661814.3662115} } -
2024
GADTs are not (even partial) functors
Pierre Cagne, Enrico Ghiorzi, Patricia Johann
Mathematical Structures in Computer Science 34(10), pp. 1079–1102.
Abstract
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 \(\mathbf{Set}\) 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 \(\mathbf{Set}\) 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 \(\mathbf{Set}\) with other categories that account for this partiality.
BibTeX
@article{CagneGhiorziJohann2024, author = {Cagne, Pierre and Ghiorzi, Enrico and Johann, Patricia}, title = {{GADTs} Are Not (Even Partial) Functors}, journal = {Mathematical Structures in Computer Science}, volume = {34}, number = {10}, pages = {1079--1102}, year = {2024}, doi = {10.1017/S0960129524000161} } -
2022
Characterizing functions mappable over GADTs
Patricia Johann, Pierre Cagne
Programming Languages and Systems (APLAS 2022), Lecture Notes in Computer Science 13658, pp. 135–154. A preprint version appeared on arXiv as How functorial are (deep) GADTs?, with Agda code.
Abstract
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 \(\mathsf G\), 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 \(\mathsf G\) precisely when it satisfies the constraints returned when our algorithm is run on \(t\) and \(\mathsf G\). This is significant: to our knowledge, there is no existing definition or other characterization of the intuitive notion of mappability for functions over GADTs.
BibTeX
@inproceedings{JohannCagne2022, author = {Johann, Patricia and Cagne, Pierre}, title = {Characterizing Functions Mappable over {GADTs}}, booktitle = {Programming Languages and Systems (APLAS 2022)}, series = {Lecture Notes in Computer Science}, volume = {13658}, pages = {135--154}, publisher = {Springer}, year = {2022}, doi = {10.1007/978-3-031-21037-2_7} } -
2020
On bifibrations of model categories
Pierre Cagne, Paul-André Melliès
Advances in Mathematics 370, article 107205.
Abstract
In this article, we develop a notion of Quillen bifibration which combines the two notions of Grothendieck bifibration and of Quillen model structure. In particular, given a bifibration \(p : \mathcal E \to \mathcal B\), we describe when a family of model structures on the fibers \(\mathcal E_A\) and on the basis category \(\mathcal B\) combines into a model structure on the total category \(\mathcal 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.
BibTeX
@article{CagneMellies2020, author = {Cagne, Pierre and Melli{\`e}s, Paul-Andr{\'e}}, title = {On Bifibrations of Model Categories}, journal = {Advances in Mathematics}, volume = {370}, pages = {107205}, year = {2020}, doi = {10.1016/j.aim.2020.107205} }
Preprints
-
2024
Early announcement: parametricity for GADTs
Pierre Cagne, Patricia Johann
Early announcement at MFPS 2024 (Mathematical Foundations of Programming Semantics). arXiv:2411.00589.
Abstract
Relational parametricity was first introduced by Reynolds for System F. Although System F provides a strong model for the type systems at the core of modern functional programming languages, it lacks features of daily programming practice such as complex data types. In order to reason parametrically about such objects, Reynolds' seminal ideas need to be generalized to extensions of System F. Here, we explore such a generalization for the extension of System F by Generalized Algebraic Data Types (GADTs) as found in Haskell. Although GADTs generalize Algebraic Data Types (ADTs) — i.e., simple recursive types such as lists, trees, etc. — we show that naively extending the parametric treatment of these recursive types is not enough to tackle GADTs. We propose a tentative workaround for this issue, borrowing ideas from the categorical semantics of GADTs known as (functorial) completion. We discuss some applications, as well as some limitations, of this solution.
In preparation
-
—
Homotopy categories of Quillen bifibrations
Pierre Cagne, Paul-André Melliès
The total category of a Quillen bifibration inherits a Quillen model structure, whose homotopy category can be constructed by two successive homotopy quotients.
-
—
Identity types as equality predicates
Pierre Cagne, Paul-André Melliès
An attempt to reconcile Lawvere's definition of equality predicates in a hyperdoctrine with the path objects that interpret the identity types of Martin-Löf type theory in categories with enough homotopical structure (Quillen model categories, Joyal's tribes, fibration categories, etc.).
PhD thesis
-
2018
Towards a homotopical algebra of dependent types
Vers une algèbre homotopique des types dépendants
PhD thesis, Université Paris Diderot (now Université Paris Cité), defended on 7 December 2018. Jointly supervised by Paul-André Melliès (IRIF) and Clemens Berger (Laboratoire J.A. Dieudonné, Nice).
Jury: 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).
Summary
Broadly speaking, my thesis is a quest for categorical structures that can interpret Martin-Löf type theories and their variants. One of the main goals is to reconcile Lawvere's view of categorical logic, developed through hyperdoctrines and related structures, with the types-as-fibrations philosophy initiated by Awodey and Warren and advocated by Voevodsky in his model of univalence in simplicial sets.
In the process, I designed a structure mixing Grothendieck bifibrations and model categories, together with a theorem that constructs such structures generically. This result can be read as a Grothendieck construction for pseudofunctors valued in the 2-category of Quillen model structures, left Quillen functors and natural transformations; for that reason, the new notion is called a Quillen bifibration. The theorem 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 behave peculiarly: they can be constructed by two successive localizations, and, oddly, both can be obtained as Quillen's homotopy quotient of a model category. The subtlety is that the intermediate model category might not have all pushouts or pullbacks: building on work by Jeff Egger, we show that Quillen's construction of the localization still goes through in that more general setting. The study of these homotopy categories suggests a variation on Grothendieck bifibrations in which (some of) the push functors are only defined up to homotopy.
The last part of the thesis uses the intuition developed through Quillen bifibrations to treat Joyal's tribes in a fibrational setting. Tribes are minimal structures to interpret homotopy type theory, reminiscent of Brown's categories of fibrant objects. From the fibrational point of view, path objects in tribes arise from "pushing" the terminal dependent type over a base type \(A\) along its diagonal. This push is of the kind mentioned above: the universal property it satisfies holds only up to homotopy. Still, this reading of tribes makes a clear connection with Lawvere's equality predicates in first-order logic (or in extensional dependent type theory): in a hyperdoctrine, the equality predicate for objects of sort \(A\) is the image (the push) along the diagonal of the total predicate on \(A\). We design a fibrational structure that generalizes tribes. To do so, we develop a framework of relative (orthogonal or weak) factorization systems: a two-level version of the usual factorization systems, from which the usual notion is recovered in degenerate cases.
BibTeX
@phdthesis{Cagne2018, author = {Cagne, Pierre}, title = {Towards a Homotopical Algebra of Dependent Types}, school = {Universit{\'e} Paris Diderot}, year = {2018}, doi = {10.70675/475f6288za6f9z4847z89d8zbfa27187f6d4} }
Talks
-
2023
GADTs are not (even lax) functors
Structure Meets Power 2023 · Boston · June 2023
Extending the results presented at TYPES 2023: GADTs cannot be interpreted as lax functors on the category of sets and partial functions either.
-
2023
Partiality wrecks GADTs' functoriality
TYPES 2023 · València · June 2023
GADTs cannot be interpreted as non-trivial functors on sets, even when the morphisms between sets are allowed to be partial functions.
-
2022
Characterizing functions mappable over GADTs
APLAS 2022 · online · December 2022
Presentation of the paper of the same name.
-
2022
Group theory without groups
Closing colloquium, HoTTEST Summer School 2022 · online · August 2022
-
2020
On the symmetries of spheres in univalent foundations Invited
HoTTEST seminar · online · November 2020
An early report on the results of the paper of the same name.
-
2020
On the symmetries of spheres in univalent foundations Cancelled
TYPES 2020 · Torino · March 2020
The conference was cancelled because of the COVID-19 outbreak.
- 2019
-
2017
When computational monads go clubbing
Category Theory 2017 · Vancouver · July 2017
As part of the Kan Extension Seminar II.
-
2016
Bifibrations of model categories
Category Theory 2016 · Halifax · August 2016
An early presentation of On bifibrations of model categories.
-
2015
Nominal sets for quantum memory: an algebraic account of linear parameters
PhD student seminar · Université Paris Diderot · October 2015
Monads with arities, used to formalize the allocation and deallocation of memory in a quantum program.
Notes
- 2022
-
2015
A semantic proof of the compactness theorem French
Notes for a talk at the student workshop on logic, 29 October 2015.
-
2014
Stacks in groupoids as homotopy limits
Preparatory notes for a talk in the course Moduli problems, stacks and simplicial presheaves taught by Gabriele Vezzosi. Following the work of Sharon Hollander, they detail how the condition for a category fibered in groupoids to be a stack can be reformulated as a descent condition.
Before the PhD
The research I did as a student at École normale supérieure and Université Pierre et Marie Curie. Most of it is written in French.
-
2015
Monade d'état quantique et ensembles nominaux French
Master's thesis (M2, MPRI), École normale supérieure. Five-month internship supervised by Paul-André Melliès.
A categorical framework, based on monads with arities, to model memory allocation and deallocation in a quantum program, and more generally in a program with linear resource management.
-
2014
Le localisateur fondamental minimal French
Master's thesis (M2) in pure mathematics, Université Pierre et Marie Curie (Paris 6), supervised by Georges Maltsiniotis.
On the proof by Denis-Charles Cisinski of a conjecture made by Grothendieck in Pursuing Stacks: every basic localizer contains the weak homotopy equivalences.
-
2013
Topos et hypothèse du continu French
First-year master's dissertation (M1), Université Pierre et Marie Curie, supervised by Emmanuel Lepage.
How Grothendieck toposes prove the independence of the continuum hypothesis from ZFC.
-
2012
Tessellation and polyomino composition
Research internship (M1, École normale supérieure), LaCIM, Université du Québec à Montréal, supervised by Srečko Brlek.
On a conjecture about the preservation of the tiling property of a polyomino under some transformations; the goal was partially achieved. The slides were presented at the workshop GTGeo 2013.
-
2011
Énumération et génération des configurations locales des plans discrets French
Research internship (L3, École normale supérieure), LORIA, Nancy, in the ADAGIo team, supervised by Damien Jamet and Éric Domenjoud.
Counting and generating the local configurations of discrete planes, with a theoretical part and a programming part.