Rencontre, 28 septembre 2023
Programme
- 10:30 – 12:00
-
William Simmons (Oxford University (UK))
The Caus[C] construction takes a base category of unnormalised processes (e.g. stochastic, quantum, or affine maps) and applies double-glueing with an orthogonality to restrict to deterministic/normalisation-preserving processes, lifting the monoidal product of C to many products representing different causal structures. Previous work by the authors has shown such categories are models of MLL and, later, BV. In this follow-on work, we devise a sound and complete logic for compatibility of causal structures with respect to composition and show it is independent of both the base category and the local system types (beyond the identification of first-order systems). This logic is a conservative extension of pomset logic with additional directed axioms, which themselves can be faithfully encoded back into pomset. Using this, we can relate a known separating statement between pomset and BV to a standard result of process matrices in quantum causality.
Joint work with Aleks Kissinger.
- 13:45 – 14:45
-
Antoine Allioux (IRIF)Invited talk: Higher Structures in Homotopy Type Theory
The definition of algebraic structures on arbitrary types in homotopy type theory (HoTT) has proven elusive so far. This is due to types behaving like spaces instead of plain sets in general with equalities between elements of a type behaving like homotopies. Equational laws of algebraic structures must therefore be stated coherently. However, in set-based mathematics, the presentation of this coherence data relies on set-level algebraic structures such as operads or presheaves which are thus not subject to additional coherence conditions. Replicating this approach in HoTT leads to a situation of circular dependency as these structures must be defined coherently from the beginning.
We break this situation of circular dependency by extending type theory with a universe of cartesian polynomial monads which, crucially, satisfy their laws definitionally. This extension permits the presentation of types and their higher structures as opetopic types which are infinite collections of cells whose geometry is described by opetopes. Opetopes are geometric shapes originally introduced by Baez and Dolan in order to give a definition of n-categories. The constructors under which our universe of cartesian polynomial monads is closed allow us to define, in particular, the Baez-Dolan slice construction on which is based our definition of opetopic type.
Opetopic types then enable us to define coherent higher algebraic structures, among which infinity-groupoids and (infinity, 1)-categories. Crucially, their higher structure coincides with the one induced by their identity types. We then establish some expected results in order to motivate our definitions.
- 15:15 – 16:15
-
Lison Blondeau-Patissier (Aix-Marseille)
As shown by Tsukada and Ong, normal (extensional) simply-typed resource terms correspond to plays in Hyland-Ong games, quotiented by Melliès’ homotopy equivalence. Though inspiring, their proof is indirect, relying on the injectivity of the relational model w.r.t. both sides of the correspondence — in particular, the dynamics of the resource calculus is taken into account only via the compatibility of the relational model with the composition of normal terms defined by normalization.
In the present paper, we revisit and extend these results. Our first contribution is to restate the correspondence by considering causal structures we call augmentations, which are canonical representatives of Hyland-Ong plays up to homotopy. This allows us to give a direct and explicit account of the connection with normal resource terms. As a second contribution, we extend this account to the reduction of resource terms: building on a notion of strategies as weighted sums of augmentations, we provide a denotational model of the resource calculus, invariant under reduction. A key step — and our third contribution — is a categorical model we call a resource category, which is to the resource calculus what differential categories are to the differential λ-calculus.
Joint work with P. Clairambault and I. Vaux-Auclair.
