The sixth edition of the LHC days will take place on Tuesday 4 and Wednesday 5 June 2024 at LS2N in Nantes.

Registration

Please use this form in order to register (submitting talks is not possible anymore). The deadline for registering is 17 May 2024.

Note that, unfortunately, we will not be able to sponsor travel or local expenses.

Location

The conference will take place in the LS2N, the precise room will be made available later on.

Invited speakers

(Provisional) program

Tuesday 4 June 2024

TBA

Wenesday 5 June 2024

TBA

Abstracts

Dimitri Ara: Construction de Grothendieck et ω-catégories de Gray

Le but de cet exposé est de présenter la construction de Grothendieck pour les ω-catégories strictes et d’expliciter ses fonctorialités naturelles dans le langage des ω-catégories de Gray, c’est-à-dire des catégories enrichies dans la catégorie des ω-catégories strictes munie du produit de Gray.

Thibaut Benjamin: Computation of inverses in weak ω-categories

Filippo Bonchi: Diagrammatic Algebra of First Order Logic

The interaction of linear and cartesian bicategories gives rise to first-order bicategories that improve Peirce’s calculus of relations in two ways: (1) their axioms provide a proof systems that is both purely equational and complete; (2) the language has the same expressivity of first-order logic. Since the proof system is purely equation and the syntax is diagrammatic proofs are exactly diagrams rewrites. In particular, our framework nicely accomodate Peirce existential graphs.

https://arxiv.org/pdf/2401.07055.pdf

Hugo Cadière: Toward a synthetic theory of modality: modalities in homotopy type theory

The main insights of modal homotopy type theory stem from E. Moggi’s categorical semantics of computer programs, which provided the first monadic interpretation of modalities. This set a first milestone towards a categorical interpretation of modalities, which was further extended by Lawvere’s work on “adjoint modalities”. Modalities play a central role in homotopy type theory, as they provide a characterization of types endowed with a factorization system, as shown in chapter 7 of the Hott book. Recent developments in Hott have also shown homotopy type theory to provide a fairly original approach to modalities, which extends to a theory of so-called “higher modalities”. In this talk, I will present the recent developments of modal homotopy type theory and compare them with other approaches to modalites in type theory and logic.

Clovis Chabertier: __

Crossed modules have been studied in various contexts for a long time in algebraic topology, beginning with the work of Whitehead in [1] to understand pointed homotopy 2 types. Loday in [2] shows that crossed modules of groups can be understood in many ways : as groups internal to the category of small categories, as simplicial groups with Moore complex of length 1, as a 1−catgroups, or as a categories internal to the category of groups. These last two descriptions allow him to generalize crossed modules of groups to higher versions, namely n-cat-groups. Morally such an object is an n-fold category internal to groups, and higher versions of crossed module, say n-crossed modules can be inductively defined as a crossed module internal to the category of (n−1)-crossed modules. The other idea of Loday is that one can associate to an n−crossed module L = H→G a space BL such that the canonical sequence BH → BG → BL is a homotopy fiber sequence. Using these ideas, he was able to prove that n-crossed modules are models for pointed homotopy (n+1)-types. Later on, several authors studied crossed modules in other algebraic contexts. For example Ellis in [3] studies n-crossed cubes of associative/commutative/Lie/etc.. algebras and proves that such objects can be equivalently defined as n-fold categories internal to algebras of the associated type. In the 00’s, Janelidze in [4] gives a general framework in which crossed modules can be defined: semi-abelian categories, and proves that the category of crossed modules internal to a semi-abelian category C is equivalent to the category Cat(C) of internal categories to C. One can play the same game and prove that n-fold crossed modules internal to C are equivalent to n-fold categories internal to C. Many algebraic categories are known to be semi-abelian : the categories of groups, non-unital rings, associative or commutative algebras, Lie algebras, etc … And it seems to be folklore that the category of algebras over a symmetric algebraic reduced operad is semi-abelian. However the definitions of Janelidze and Ellis are not so well adapted to the case of algebras over an operad. First of all, their definitions are a bit involved, Indeed they both required lots of axioms. For example, a crossed module of associative algebras is the data of a morphism of algebras d : A → B, an internal action of B on A such that d is equivariant and satisfies a “Peiffer” condition. When one wants to go to higher crossed modules, this becomes awful. Second, the homotopical properties, and especially the link between (higher) crossed modules of algebras and the homotopy theory of algebras over an operad is not clear at all. In a current work, Leray-Rivière-Wagemann (LRW) give yet another definition of crossed modules of algebras over an operad P, namely it is the data of a P-algebra structure on a chain complex …0 → A→ B concentrated in degrees 0 and 1. This has two main advantages over the previous definitions. First it is a very concise and clear definition. Second it is clearly linked to the homotopy theory of P-algebras, that is differential graded P−algebras.

In an upcoming series of two papers, we generalize the definition of LRW to get a very concise definition of crossed n-cube of algebras over an operad, namely it is the data of a P−algebra structure on an n−fold chain complex $A_{•,…,•}$ concentrated in degrees $(ε_1, …, ε_n)$, $ε_i ∈ {0, 1}$. We prove that such a structure descends to $P$−algebra structures on each $A_{ε_1,…,ε_n}$, and that we get a crossed n-cube of algebras in the sense of Ellis. We also prove that our category of crossed $n$-cubes of $P$−algebras is equivalent to the category of $n$−fold categories internal to the category of $P$−algebras, so our definition is equivalent to the ones of Ellis and Janelidze. The main advantage of our “global” definition as opposed to the previous “locals” ones lies in the existence of the monoidal functor Tot : Ch(…Ch(A)) → Ch(A) as soon as A is a monoidal abelian category, for example A = Q-Vect. In particular it induces a functor which sends a crossed n−cube of P-algebras (in our sense) to a differential graded P-algebra concentrated in degrees $0, …, n + 1$, so here the link with the homotopy theory of $P$-algebras is almost for free.

The second paper of this series is devoted to an application to rational homotopy theory and especially to a conjecture of Félix and Tanré in [?]. In this paper they construct a crossed module of groups C(g) associated to a complete differential graded Lie algebra g concentrated in degrees 0 and 1. They prove that the classifying space $BC(g)$ of this crossed module is isomorphic to the geometric realization ⟨g⟩ of g in the sense of [6] and conjecture that given a cdgl concentrated in degrees 0, …, n, one can associated to it a n-cat-group and that its classifying space is isomorphic to the geometric realization of this Lie algebra. We studied the case $n = 2$ and prove that for a Lie algebra in square g, one can associate $Tot(g)$ a complete dgLie algebra of height 3 and its geometric realization $⟨Tot(g)⟩$. Or one can associate a crossed square of groups and consider its classifying space. We prove that thoses two constructions are weakly homotopy equivalent.

References

[1] A. Whitehead, combinatorial homotopy. II, Appl. Categ. Structures 25 (2024), no. 2, 1159–2076.
[2] J-L. Loday, Spaces with finitely many non-trivial homotopy groups, Journal of Pure and Applied Algebra, vol. 24, 1982, 179-202, https://doi.org/10.1016/0022-4049(82)90014-7.
[3] G-J. Ellis, Higher dimensional crossed modules of algebras, Journal of Pure and Applied Algebra, vol. 52, 1988, 277-282, https://doi.org/10.1016/0022-4049(88)90095-3
[4] G. Janelidze, Internal Crossed Modules, Georgian Mathematical Journal, vol. 10, no. 1, 2003, pp. 99-114. https://doi.org/10.1515/GMJ.2003.99
[5] Y. Félix, D. Tanré, Realization of Lie algebras and classifying spaces of crossed modules, Algebr. Geom. Topol. 24 (2024) 141-157, https://doi.org/10.2140/agt.2024.24.141
[6] U. Buijs, Y. Félix, A. Murillo, D. Tanré Lie Models in Topology, Springer Nature Switzerland AG 2020, https://doi.org/10.1007/978-3-030-54430-0

Cole Comfort: A phase-space approach to rewriting infinite-dimensional quantum circuits

The ZX-calculus is a family of graphical languages used to reason about linear maps between finite-dimensional Hilbert spaces. However, the ZX-calculus is by no means bound to Hilbert spaces! By tracking the nondeterministic evolution of discrete position and momentum operators, we show that the stabiliser ZX-calculus can be represented in terms of affine Lagrangian relations over finite fields. In other words, we give a phase-space description of the stabiliser ZX-calculus. Unlike the Hilbert space semantics, this generalises naturally to infinite dimensions: by considering a subcategory of affine Lagrangian relations over the complex numbers, we obtain a ZX-calculus for Gaussian quantum circuits with Dirac deltas. This tracks the nondeterministic evolution of multivariate Gaussian probability distributions between continuous-variable position and momentum operators, which is not possible in Hilbert spaces. Complete equational theories are provided for both the finite and infinite dimensional semantics.

This is based on joint work with Titouan Carette and Robert I. Booth:
https://arxiv.org/pdf/2401.07914
https://arxiv.org/pdf/2403.10479

Thomas Ehrhard: TBA

TBA

Uli Fahrenberg : Presenting Interval Pomsets with Interfaces

We develop a presentation of interval-order partially ordered multisets with interfaces (ipomsets) as generated by a graph of certain discrete ipomsets (starters and terminators) under the relation which composes subsequent starters and subsequent terminators. Using this presentation, we show that also subsumptions are generated by elementary relations. We develop a similar correspondence on the automata side, relating higher-dimensional automata and ST-automata.

Arnold Grigorian : Meta-mathematics and Internalization of Logic in Category Theory

The talk will be dedicated to the notion of internal language in category theory and the philosophical intuition behind it, as well as examples of its practicle use for obtaining certain results. I will first consider the evolution of how this notion of internal logic evolved, from 1970s (in MacLane’s articles and others) and its informal presentation to a more rigorous one, like in, e.g., Johnstone’s book on topos theory, and, finally, to its use in recent developments. Since certain categories with rich enough structure (like various kinds of topoi) can be used as a model of a “mathematical universe”, one can differentiate the use of the internal language of the category in question, i.e., “reasoning inside the universe”, with what we will call meta-reasoning or external reasoning (which is actually more similiar the ordinary style of mathematical reasoning), i.e., “reasoning about the universe”. The relation between the external and internal reasoning is often swept under the carpet. I’ll try to clarify the relation between the two modes in question and provide certain examples where approaching a certain issue ‘externally’ vs. ‘internally’ yields different results (or, in contrast, the same). In general, the internal language of a certain category is constructive, i.e., the axiom of choice doesn’t hold internally. Thus, reasoning internally can prevent making unwarranted statements. For example, in The Simplicial Model of Univalent Foundations (after Voevodsky) (2018) where the ambivalent logic is classical (an observation made by T. Coquand) as opposed to the internal constructive reasoning, making the obtained result partially illegitimate “internally”.

Sources:

Caramello, O. (2018). Theories, sites, toposes: Relating and studying mathematical theories through topos-theoretic “bridges” (First edition). Oxford University Press. Chapter 7 “Internal category theory”. (1998). In Studies in Logic and the Foundations of Mathematics (Vol. 141, pp. 407–440). Elsevier. https://doi.org/10.1016/S0049-237X(98)80037-2
Gauthier, Y. (2015). Towards an Arithmetical Logic: The Arithmetical Foundations of Logic. Springer International Publishing. https://doi.org/10.1007/978-3-319-22087-1
Jacobs, B. (1999). Categorical logic and type theory (1st ed). Elsevier Science.
Kapulkin, C., & Lumsdaine, P. L. (2018). The Simplicial Model of Univalent Foundations (after Voevodsky) (arXiv:1211.2851). arXiv. http://arxiv.org/abs/1211.2851
Koslow, A., & Buchsbaum, A. (Eds.). (2015). The Road to Universal Logic: Festschrift for the 50th Birthday of Jean-Yves Béziau Volume II. Springer International Publishing. https://doi.org/10.1007/978-3-319-15368-1
Maclane, S. (1975). Sets, Topoi, and Internal Logic in Categories. In Studies in Logic and the Foundations of Mathematics (Vol. 80, pp. 119–134). Elsevier. https://doi.org/10.1016/S0049-237X(08)71946-3
Osius, G. (n.d.). The internal and external aspect of logic and set theory in elementary topoi.
Rijke, E., & Spitters, B. (2015). Sets in homotopy type theory. Mathematical Structures in Computer Science, 25(5), 1172–1202. https://doi.org/10.1017/S0960129514000553
Shulman, M. A. (2010). Stack semantics and the comparison of material and structural set theories (arXiv:1004.3802). arXiv. http://arxiv.org/abs/1004.3802

Nohra Hage: Combinatorics of super tableaux over signed alphabets.

We are interested on the combinatorial study of super Young tableaux over signed alphabets of any order. We introduce super Robinson–Schensted–Knuth correspondences between signed two-rowed arrays and pairs of super Young tableaux over signed alphabets. Moreover, we introduce the notion of super Schur functions and give combinatorial descriptions of the super Littlewood–Richardson coefficient for expressing a product of two super Schur functions as a linear combination of super Schur functions.

Elies Harington: Polynomials in homotopy type theory

Polynomials can be defined in any category with pullbacks, and offer a nice setting to talk about inductive types in type theory (where they are also known as containers) and planar (colored) operads, among other things. Polynomials in higher categories allow the introduction of more symmetric structures, such as some quotient types and symmetric operads. In the setting of Homotopy Type Theory, we show that polynomials in Types are morphisms in a Kleisli category on spans of types, and form the non-linear part of a linear-non-linear adjunction that makes polynomials into a (homotopical) model of linear logic. We also compare this result with an analogue construction with profunctors and generalized species of structure.

Hugo Herbelin: _Where is β-equality hidden in elementary topos? _

Elementary toposes are known to have the logical strength of Higher Order Logic which itself has the logical strength of System Fω. More precisely, elementary toposes add propositional extensionality, functional extensionality and unique choice to a variant of Fω with product types and subset types.

We propose to investigate elementary toposes from a Curry-Howard perspective, extracting out extensionality by classifying monomorphims rather than subobjects so that the resulting classifier of fibered-presented propositions into indexed-presented propositions defines only a non-extensional impredicative hProp. We’ll then explore where to find β-equality in the topos structure for conjunctions, disjunctions and quantifiers, as well as for sums and dependent products.

Peter Hines: Some algebraic & number-theoretic interpretations of associahedra

From their origins in algebraic topology, J. Stasheff’s associahedra now occur in multiple seemingly disjoint fields. This talk simply aims to add more connections to an already long list. We describe how associahedra have interesting connections to some well-established number theory, group theory, and inverse semigroup theory, and make the case that such connections are deeply categorical.

Our starting point is a labelling of the facets of associahedra by P. Erdos’s “exact covering systems” (i.e. pair-wise disjoint sets of modulo classes whose union is the whole of the natural numbers). Based on a connection between some early number-theoretic work of G. Cantor and his later set-theoretic considerations, we demonstrate that distinct facets of associahedra correspond to distinct (ordered) exact covering systems.

Such dissections of a countably infinite set are known to be related to an important class of inverse monoids (Nivat & Perot’s “polycyclic inverse monoids” – also known to linear logicians as “Dynamical Algebras”). We use this connection to label the facets of associahedra by realisations of polycyclic monoids as partial linear injections on the natural numbers.

This allows us to describe maps between distinct facets of the same associahedron in similar terms. Mappings between facets of the same associahedron are elements of Stefan Kohl’s `Class Transposition’ group, and therefore congruential bijections in the sense of J. Conway’s 1972 proof of undecidability in elementary arithmetic. We observe Conway’s motivating example occurring as a mapping between facets of the simplest non-trivial associahedron. A neat relationship between mappings between facets, and embeddings of associahedra into higher-dimensional associahedra, then demonstrates that Conway’s motivating example occurs in all dimensions.

We also consider the special case of the 1-skeleton of associahedra, and identify mappings between facets as giving a realisation of Richard Thompson’s group F. This allows us to express the elements of Thompson’s group in terms of the simple arithmetic problems that motivated Conway.

Finally, we give an entirely categorical interpretation. The congruential bijections that map between facets of a given associahedron are components of natural isomorphisms between functors. The functors in question are unbiased analogues of monoidal tensors (i.e. the setting with one “tensor” of each arity), with the binary case being familiar from linear logic. The above algebraic uniqueness results allow us to give to give a posetal functor groupoid that is an unbiased version of MacLane’s posetal monoidal groupoid W, from the original proof of his coherence theorem for associativity.

We thus identify the algebraic and number-theoretic aspects of associahedra as forms of categorical coherence.

Tom Hirschowitz: A semantic notion of inference rule for (dependent, quantitative) type theory

Type theory is a family of formal systems ranging from programming language semantics to the foundations of mathematics. In practice, type theories are defined by means of “inference rules”. Everyone in the community understands them to some extent, but they do not have any commonly accepted rigorous interpretation. Or, rather, they have several interpretations, none of which is entirely satisfactory.

In this work, after a brief overview of the literature, we introduce a rigorous, semantic notion of inference rule, our thesis being that most syntactic inference rules written in practice may be directly interpreted in this framework. If time permits, we will sketch how this covers quantitative type theories.

This is joint work in progress with André Hirschowitz and Ambroise Lafont.

Axel Kerinec: Towards Categorical Structures for Operational Game Semantics

Operational game semantics interprets λ-terms as labelled transition systems (LTS), representing interactions with the environment. The design of the transitions of this LTS is based on the analysis of normal forms of λ-terms. Compared to standard denotational game semantics composition is not a primitive notion. But it is needed in order to obtain categorical structures on such models and have a formal connection with traditional denotational game semantics.

In this talk we will present this categorical composition as well as the challenges encountered to define it.

Yves Lafont: TBD

Louise Leclerc: Several approaches to opetopes.

Kenji Maillard: Glueing Booleans for Greater Extensionality

Categorical proof of normalisation-by-evaluation (NbE) for the simply typed λ-calculus with extensional sums utilize sheaves over a category of renamings to show the existence of a normal form. Aiming for a similar result applying to a dependent type theory with extensional booleans, this presentation will revisit the construction of the site of renamings and present a synthetic construction of the first steps towards a normalization procedure inside a proof assistant.

Tanguy Massacrier: Single-set cubical categories and their formalisation with a proof assistant

We introduce a single-set axiomatisation of cubical ω-categories, including connections and inverses. We justify these axioms by establishing a series of equivalences between the category of single-set cubical ω-categories, and their variants with connections and inverses, and the corresponding cubical ω-categories. We also report on the formalisation of cubical ω-categories with the Isabelle/HOL proof assistant, which has been instrumental in finding the single-set axioms.

https://arxiv.org/abs/2401.10553

Paul-André Melliès: Transition-based template games

Simon Mirwasser : Indexed differential linear logic and Laplace transform

Differential linear logic (DiLL) is an extension of linear logic where one can interpret the differential of a function. Our aim is to refine this logic, in order to interpret linear partial differential equations, with their solutions and their parameters. To do so, we work in a graded setting: the exponential connectives are indexed by elements of an algebraic structure. In recent works, Kerjean and Lemay have shown that the Laplace transform has a crucial role in the denotational semantics of DiLL. Here, we express how this transformation changes the indexes of the exponential connectives, and thus acts on the differential operators. This gives us a framework, graded by two semirings, where we hope to be able to interpret the promotion rule. This is joint work with Marie Kerjean and Yoann Dabrowski.

Vincent Moreau: A fibrational approach to regular languages of lambda-terms

Regular languages of lambda-terms have been introduced by Salvati using denotational semantics. They extend the usual regular languages of words and trees to the higher-order setting and permit to use the compositional aspects of the lambda-calculus. In this talk, we revisit the notion of regular languages and present a fibrational setting that permits to establish in a slick and principled way some of their properties. This sheds new light on the fact that regular languages are stable by pullback but not by pushforward.

This is joint work with Paul-André Melliès.

Hugo Paquet: Element-free probability distributions and random partitions

An “element-free” probability distribution is what remains of a probability distribution after we forget the elements to which the probabilities were assigned. These objects naturally arise in Bayesian statistics, when elements are used as labels and their specific identity is not important. I will discuss the foundations of element-free distributions in terms of multisets and category theory. In particular I will explain the two main operations for moving between element-free distributions and ordinary distributions. I will then explain how we can use this theory to give a new categorical proof of Kingman’s theorem, a well-known representation theorem for infinite random partitions. (This is joint work with Victor Blanchi.)

Colin Riba: Finitely accessible arboreal adjunctions and Hintikka formulae.

Arboreal categories provide an axiomatic framework in which abstract notions of bisimilarity and back-and-forth games can be defined. They act on extensional categories, typically consisting of relational structures, via arboreal adjunctions. In the examples, equivalence of structures in various fragments of infinitary first-order logic can be captured by transferring bisimilarity along the adjunction. In most applications, the categories involved are locally finitely presentable and the adjunctions finitely accessible. Drawing on this insight, we identify the expressive power of this class of adjunctions. We show that the ranks of back-and-forth games in the arboreal category are definable by formulae à la Hintikka. Thus, the relation between extensional objects induced by bisimilarity is always coarser than equivalence in infinitary first-order logic. Our approach relies on Gabriel-Ulmer duality for locally finitely presentable categories, and Hodges’ word-constructions.

J.w.w. Luca Reggio.

Luigi Santocanale: Complete congruences of completely distributive lattices

All of the binomial lattices embed into the quantale $Q(I)$ of sup-preserving endomaps of the unit interval. Elements of this quantale can be seen as continuous monotone paths from $(0,0)$ to $(1,1)$. This quantale is in particular a completely distributive lattice. We give a description of the complete congruences of completely distributive lattices by means of an interior operator on the collection of the closed sets of an associated topological space. In particular, we show that these form a frame. We give a description of this frame for the unit interval lattice. We show that this is not a Boolean algebra nor it is a (co)spatial frame. For the quantale $Q(I)$, we give a geometrical interpretation of these congruences by means of directed homotopies.

Participants

  1. (CNRS)
  2. (IRPHIL / Université Jean Moulin lyon 3)
  3. (Nantes Université)
  4. (I2M (Institut de Mathématiques de Marseille) AMU (Université d’Aix-Marseille))
  5. (ENS - PSL)
  6. (Université d’Aix-Marseille)
  7. (Nantes Université (LMJL))
  8. (LMJL - Nantes Université)
  9. (Dept. of Mathematics, University of York, U.K.)
  10. (Università di Bologna)
  11. (Université Claude Bernanrd Lyon 1)
  12. (University of Pisa)
  13. (Université de Nantes)
  14. (Inria)
  15. (LAMA, CNRS, Univ. Savoie Mont Blanc)
  16. (University of Cambridge)
  17. ()
  18. (Vrije Universiteit Amsterdam)
  19. (Institut Catholique de Lille)
  20. (IRIF)
  21. (IRIF, Université Paris Cité, Inria Paris)
  22. (CNRS-UPC)
  23. (LIP – ENS de Lyon)
  24. (Inria)
  25. (LIP – ENS de Lyon)
  26. (IMJ-PRG)
  27. (IRIF, Université Paris Cité)
  28. (Inria, IRIF, CNRS, Université Paris-Cité)
  29. (Ecole Polytechnique)
  30. (Université Jean Moulin Lyon 3)
  31. (Université Jean Moulin Lyon 3)
  32. (LIPN)
  33. (IRIF)
  34. (LIS/AMU)
  35. (IRIF)
  36. (INRIA )
  37. (ENS student)
  38. (Université de Lorraine, CNRS, Inria)
  39. (LIPN)
  40. (LACL)
  41. (LIP-PLUME)
  42. (Inria)
  43. (– (due to russian affiliation))
  44. (Inria - IRIF)

Contacts

In case of any question you can contact the organizers Assia Mahboubi and Nicolas Tabareau (local organizers), Samuel Mimram and Lionel Vaux (LHC coordinators).

Support