Program - PSSL 109

Kamerlingh Onnes Building (room A0.51)

Leiden University, The Netherlands

Fotos: @Fromourdot - ©Jelle Mes

Friday

14:00–14:20 Opening

(co)monads

14:20–14:40 Quentin Aristotle: monotone weak distributive laws over the lifted powers monad in categories of algebras.

Noticing the similarity between the monotone weak distributive laws combining two layers of nondeterminisms in sets and in compact Hausdorff spaces, we study whether the latter law can be obtained automatically as a weak lifting of the former. This holds partially, but does not generalize to other categories of algebras: we then characterize when exactly monotone weak distributive laws over powerset monads in categories of algebras exist, exhibiting a law combining probabilities and non-determinism in compact Hausdorff spaces and showing on the other hand that such laws do not exist in a lot of other cases.

14:40–15:00 Soichiro Fujii: monad theory through enrichment.

We shed new light on two classical results in the theory of monads, namely Beck's monadicity theorem and Linton's theorem (characterizing the Eilenberg-Moore category of a monad as a suitable pullback of the presheaf category over the Kleisli category along the Yoneda embedding of the base category), through bicategory-enriched category theory. Using bicategories that capture categories over a fixed category C as enriched categories, we characterize the Eilenberg-Moore category of a monad T on C as a free cocompletion of the Kleisli category of T (with respect to a suitable class of weights). This characterization yields Beck's monadicity theorem, and a general description of the free cocompletion gives rise to Linton's theorem. This talk is based on ongoing joint work with John Bourke.

15:00–15:20 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 a 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.

Joint work with Luca Reggio.

15:20–15:40 Miloslav Štěpán: some characterizations of lax idempotency for pseudomonads.

In this talk we will discuss various equivalent conditions for lax idempotency of a pseudomonad.

The first one involves a 2-functor associated to any pseudomonad that sends left adjoints to the compo- nents of the pseudomonad’s unit to colax algebras. A pseudomonad is lax-idempotent if and only if this 2-functor restricts to an isomorphism between reflectors and normal colax algebras.

The second one involves a “lax idempotentiation” process that can be applied to any 2-monad on a suitable 2-category – it is a higher-dimensional analogue of (Sabah Fakir, Monade idempotente associ´ee `a une monade) that can be used to turn (suitable) 2-monads into lax-idempotent ones. A 2-monad is lax-idempotent if and only if this construction can be applied to it and at the same time does nothing to it.

The third one involves colax adjunctions and the pseudomonad’s Kleisli 2-category. A pseudomonad on a 2-category K is lax-idempotent if and only if any biadjunction between K and some other 2-category L whose left biadjoint factorizes through its Kleisli 2-category “descends” to a colax adjunction between the Kleisli 2-category and L.

We also describe how these results specialize to characterizations of idempotent 1-monads. If time permits, we will also mention the relationship of lax-idempotency of a pseudomonad and the presence of certain (enriched weak) colimits in its Kleisli 2-category.

The results in the first and second paragraph may be found in the author’s recent PhD thesis currently awaiting a review. One direction of the result in the third paragraph may be found either in the thesis or in the author’s arXiv preprint.


15:40–16:00 20 minute coffee break

16:00–17:00 Maaike Zwart: my hobby, self-distributing monads.

I will look at the special case of finding distributive laws for monads over themselves.

Monads model computational effects, and distributive laws show the interaction between computational effects when one effect is applied on top of another, that is, if their monads are composed. Self-distribution of monads then corresponds to having two layers of the same effect, which comes up remarkably often in practice.

Distributive laws can be quite hard to find, and might not exist at all. The special case of self-distributions looks much easier at first glance, but is it really? A second glance makes them look much harder, or at least, much more confusing and fiddly than distributing two distinct monads. In the end, I will show why self-distribution is really no different from distributing two non-identical monads over each other.

Studying self-distributions has turned into my hobby. Even though finding self-distributive laws (or proving that they don't exist) is technically the same as studying distributive laws in general, self-distributions tend to spark the right ideas, and steer research into the right direction. So join me for a fun and lighthearted exploration of self-distributions.

Saturday

monoidal categories

11:30–11:50 Paul Blain Levy: strictifying monoidal structure, revisited.

Schauenburg claimed that, on a category of structured sets, any monoidal structure is isomorphic to a strict one. Unfortunately, the proof given was slightly incorrect (due to an issue with the empty set), but it can be adapted to work in two special cases, including many examples of interest. The first case is where the monoidal operation preserves emptiness in each argument; and the second is where it reflects emptiness in each argument (with some extra conditions). Consequently, on Set, every monoidal structure is isomorphic to a strict one. Whether this is the case for Set^2 remains open.

11:50–12:10 Tomas Perutka: generalized Fox’s Theorem and pseudocommutativity.

Classically, Fox’s theorem tells us that for a symmetric monoidal category C, the category CMon(C) of commutative monoids in C and homomorphisms admits finite coproducts. We can observe a certain pattern: we are considering commutative monoids in C, which is itself a commutative pseudomonoid in the 2-category Cat. We propose a vast generalization of Fox’s result stated in the language of Lawvere 2-theories: symmetric monoidal categories are replaced by models of a 2-theory T in Cat, and instead of commutative monoids, we refer to internal algebras in a model. For all this to make sense, we define a notion of pseudocommutativity for Lawvere 2-theories using the Gray tensor product – which both matches and simplifies the standard definition in the setting of 2-monads. This is a work in progress, joint with John Bourke.

12:10–12:30 Noam Zeilberger: context-free grammars and finite-state automata over categories.

I propose to talk about joint work with Paul-André Melliès developing a categorical perspective on context-free grammars and finite-state automata, which grew out of our line of work on type refine- ment systems. The starting point of that earlier work was to consider type systems fibrationally as functors from a category of typing derivations to a category of terms, so that typing is reduced to a “lifting problem” along the functor. In the talk I will explain how both parsing by a context-free grammar (CFG) and recognition by a nondeterministic finite-state automaton (NFA) may be similarly expressed as lifting problems along certain kinds of functors, and argue that viewing CFGs and NFAs this way seems to have some real explanatory power.

A generalized CFG is a functor from a free colored operad (aka multicategory) generated by a pointed finite species into an arbitrary base operad: this encompasses classical CFGs by taking the base to be a certain operad constructed from a free monoid, as an instance of a more general construction of an operad of spliced arrows WC for any category C. A generalized NFA is a functor from an arbitrary bipointed category or pointed operad satisfying the unique lifting of factorizations and finite fiber properties: this encompasses classical word automata and tree automata without ϵ-transitions, but also automata over non-free categories and operads. We show that generalized context-free and regular languages satisfy suitable generalizations of many of the usual closure properties, and in particular we give a simple conceptual proof that context-free languages are closed under intersection with regular languages.


12:30–13:40 70 minute lunch break

13:40–14:40 Paolo Perrone: notions of expectation and probability monads.

Probability theory is a quantitative theory.

Numbers, as opposed to points of an arbitrary space, play a prominent role in probability, beceause:
- First of all, probability itself is modeled as a number, between 0 and 1;
- The most common application of probability theory are about predicting numbers, such as prices or outcomes of noisy measurements.
This focus on numbers has made categorical treatments of probability quite difficult in the past few decades. However, in the past few years, the community has made significant progress by treating the quantitative nature of probability as a feature, and by modeling categorically precisely these "numerical" aspects.

Here is one such idea. When we deal with random numbers, as opposed to points of an arbitrary space, we can perform what is arguably the most important operation of probability: expectation. It has the intuition of "averaging a random variable over our uncertainty", and it has a number of applications, which we can interpret categorically:
- When the number that we are averaging is a probability, we can interpret the average as a composition of probabilities, and this idea leads to probability monads and categories of kernels;
- When we are averaging an arbitrary quantity, we are replacing a probability distribution with a canonical element, or result. This leads to algebras of probability monads.
We will explore these ideas in detail, and show the probabilistic significance of the relevant universal properties.
Given time and interest, we can also abstract these ideas further, using the language of Markov categories.
No previous knowledge of probability theory is assumed.


14:40–14:50 10 minute coffee break

enriched and multi categories
14:50–15:10 David Forsman: multicategorical meta-theorem and the completeness of restricted algebraic logics.

Consider the classical Eckmann-Hilton argument: if a set carries two unital magma structures that distribute over each other, then these structures coincide and determine a single commutative monoid. This argument extends from sets to symmetric multicategories, but why? More generally, when do equational proofs in sets lift to categorical settings?

We answer this question through the Multicategorical Meta-Theorem. We identify precisely eight subcategories ∆ of FinOrd of finite ordinals and functions, each corresponding to a coherent structure that can be added to a monoidal category (like symmetry, deletion, or duplication). For six of these structures — including symmetric multicategories and cartesian multicategories — we prove that if E ∪ {ϕ} is an ∆–theory and the equation ϕ follows from the set of equations E in Set, then ϕ follows from E in any model in any ∆-multicategory.

We prove the Multicategorical Meta-Theorem by restricting the equational deduction system ⊢ into ⊢∆ for eight different structures ∆ and prove categorical soundness and completeness theorems. Exactly six of the eight deduction systems ⊢∆ have completeness in sets. Completeness in set-based models and soundness in all models yields the meta-theorem.

In addition, a corollary of our result is that if T ∪ {ϕ} is an algebraic ∆-theory and ∆ is one of the six structures, then T ⊢ ϕ if and only if T ⊢∆ ϕ. This shows that in certain cases one may simplify the proof search without sacrificing the completeness.

15:10–15:30 Ruben Mud: betweenness in enriched categories.

The idea that a point can be between two other points is ubiquitous throughout mathematics. Commonly this is modelled with a ternary relation. In this talk, we argue that betweenness is intrinsic to the theory of enriched categories. More precisely, every betweenness relation induces an enriched category, and every enriched category comes with a betweenness relation. It turns out that this shift in interpretation is functorial.

15:30–15:50 Henning Basold: towards formal, enriched and homotopical coalgebra.

Coalgebra, the study of system behaviour with its resulting reasoning methods, has found many applications in computer science. However, in many systems one needs either more information or has to relax the homomorphism condition for coalgebras. In this talk I will particularly focus on relaxing the homomorphism condition to commutativity up to (coherent) homotopy, and on achieving this via topological enrichment to enable computations in concrete cases. To avoid redeveloping the theory of coalgebra anew for all cases, I will introduce a formal theory of coalgebra formulated in fibrant double category, which are double categories where pro-morphisms can be lifted along morphisms (also known as framed bicategories or equipments). The resulting theory generalises existing results for coalgebra in on poset-enriched categories and fibrations.


15:50–16:00 10 minute coffee break

categorical logic
16:00–16:20 Lingyuan Ye: incompleteness and intentionality via universal property of arithmetic.

This talk proposes an approach towards understanding incompleteness phenomena from the perspective of categorical logic. The upshot is that incompleteness theorems of arithmetic are canonical consequences of, as the title suggests, universal properties of various arithmetic theories. From a technical point of view, this approach promises a completely categorical proof of incompleteness, without needing the tedious syntactic details of the arithmetisation process, which usually depends on too many arbitrary choices. Philosophically, the universal property also demystefy a lot of intensional claims often exhibted in either the proof or the statement of incompleteness results in logic — they actually have numerous “counterexamples”, including the second incompleteness theorems, if not stated carefully enough. This is yet another great example of categorical method providing both techinically and philosophically more satisfying answers to foundational aspects of logic itself.

16:20–16:40 Julia Morin: Joyal’s representation theorem for Heyting categories.

An unpublished result by André Joyal, believed to have been formulated around 1970, extends the Stone representation theorem for Boolean algebras to Heyting categories. Specifically:

Every small Heyting category H can be embedded into one of the form SetC via a Heyting, conservative functor.

Through the construction of syntactic categories built from first-order theo- ries, Joyal’s representation theorem offers completeness results for intuitionistic first-order logic. While a model-theoretic proof was originally presented by Makkai and Reyes in 1977, we introduce in this work a new, purely categorical approach.

16:40–17:00 Alex Simpson: countable and dependent choice and countably distributive toposes.

The axiom of countable choice and the stronger axiom of dependent choice are frequently used in mathematics, both classical and constructive. I shall consider various formulations of these axioms in elementary toposes and in Grothendieck toposes. One interesting case is that of atomic toposes, for which the two choice axioms can be related to simple conditions on the base category.

Countable choice can be viewed as a special case of a full countable distributivity property, enjoyed by countaby distributive toposes. I shall define this notion, provide several examples, and show that it enjoys a number of interesting characterisations.

An early incarnation of the material in the first half of the talk appeared in the master’s dissertation of my former student Severin Mejak. While much of this material may be folklore, I shall give a systematic presentation, which will serve the purpose of setting the scene for the second half of the talk.


conference diner

Sunday

type theory and higher categories

11:30–11:50 Mark Williams: presentations of topological modalities in homotopy type theory.

Homotopy type theory (HoTT) is an internal language for (∞, 1)-topoi and as such we are able to right down the notion of a subtopos of the ambient universe. In particular we can describe those which come from a topology: the so called topological modalities.

In this work we introduce a notion of presentation for a topological modality, to more directly encode the choice of Grothendieck topology. Using these, and exploiting homotopy theoretic ideas, we are able to recover internal n-dimensional sheaf conditions for n-truncated types. For each external natural number we are able to show this corresponds to the usual sheaf condition. By placing the additional hypothesis that all objects in the presentation are projective we are further able to describe explicit sheafification of −1-truncated types and can recover some Kripke-Joyal style reasoning. We derive a “local choice” axiom and obtain results about how cohomology in the subtopos relates to cohomology in the base universe.

We apply these results to an extension of HoTT axiomatising the internal logic of the classifying topos of an algebraic theory. In this setting we can derive the axioms for synthetic algebraic geometry and simplify a proof that the interval is simplicial in synthetic category theory.

11:50–12:10 Matteo Spadetto: higher dimensional semantics of propositional dependent type theories.

In the study of the semantics of dependent type theory, we typically encounter two distinct, but related, approaches: syntactical and categorical. The syntactical approach di- rectly mirrors the structure of the syntax of the theory, via a choice function that defines how judgements in the conclusions of inference rules are interpreted based on the interpretations assigned to the premises. On the other hand, the categorical approach adds structure and property to the model: structure and property that allows to recover a choice function analogous to that provided in the syntactical approach. For instance, assuming that the notion of equality of a given theory is extensional, the inference rules of the dependent sum type constructor correspond to the requirement that the family of display maps in a model is closed under composition up to isomorphism: this categorical property encodes into the model the syntax of dependent sums.

However, in case we drop the extensionality of the identity types, such a simple and clear characterisation of the type constructors is harder to find, and hence a (1-dimensional) categorical presentation of the semantics of such a theory is not completely satisfactory. Given this challenge of encoding intensional theories into 1-dimensional categorical terms, a challenge that persists even for propositional theories — i.e. very intensional theories, also known in the literature as axiomatic, weak, objective theories — in this talk we adopt Garner’s perspective to study the semantics of propositional theories from a higher categorical point of view, specifically a 2-categorical one.

A propositional theory is a depen- dent type theory whose computation rules consist of propositional equalities, rather than the definitional equalities that normally characterise the reductions and the expansions in formal systems like Martin-Löf type theory or the calculus of constructions. Starting from the syntax of a propositional theory, we prove that its type constructors can be encoded into natural 2-dimensional category theoretic data. We use these data to show that the semantics of propositional theories of dependent types admits a presentation via 2-categorical models called display map 2-categories. In other words, we show that display map 2-categories with such data are sufficient to reconstruct the semantic counterpart of propositional theories as in the syntactical approach, particularly inducing appropriate display map categories — i.e ordinary models. It turns out that the 2-categorical requirements identi- fied by Garner for interpreting an intensional theory, in the propositional case are relaxed. Therefore, we obtain a notion of semantics for propositional theories that generalises Gar- ner’s one for intensional ones. We compare the class of models according to this notion of semantics with the class of those derived from the usual notion of semantics.

12:10–12:30 Stiéphen Pradal: a study of Kock’s fat Delta.

The study of higher categories involves many tools based on the simplex category ∆ and simplicial methods. Indeed, ∆ enables the encoding of coherences in geometric shapes for higher structures. However, the degeneracy maps in ∆ encode the identity structure strictly in contrast to the associativity structure. The category referred by fat Delta, denoted ∆ and first introduced by Kock as the category of relative finite semiordinals (i.e. relative finite ordinals with a total strict order relation), was developed as a means of providing a geometric interpretation of weak identity arrows in higher categories. Since then, it has been studied further by Paoli and, in both cases, their research was motivated by the investigation of Simpson’s conjecture in low dimensions. For different motivations related to Homotopy Type Theory (HoTT), Kraus and Sattler constructed and studied a direct replacement of ∆, that turns out to be a variation of ∆ . The background is that, internally to a type theory, it is unknown how to represent presheaves on a category in general, but presehaves on a direct category have a natural representation via type families.

We present a comprehensive study of ∆ mainly via the theory of monads with arities, which offers an abstract setting to produce nerve theorems and study Segal conditions. The primary notion in our work is that of a relative semicategory; the latter is similar to the one of relative categories without requiring identity structure, and we denote the category of relative semicategories by RelSemiCat. Our first main result is the nerve theorem for relative semicategories.

Theorem 1. Let RelGraph denote the category of relative directed graphs and let j : ∆0 → ∆ be the inclusion of the wide subcategory of relative semiordinals and relative graph morphisms. The nerve functor N : RelSemiCat → b∆ is fully faithful. The essential image is spanned by the presheaves whose restriction along j belong to the essential image of N 0 : RelGraph → c∆0.

In particular, this indicates that ∆ is for relative semicategories what ∆ is for categories. We obtain Theorem 1 by proving that the free relative semicategory monad on RelGraph is strongly cartesian in the sense of (Mark Weber, Familial 2-functors and parametric right adjoints). This is achieved by showing that the monad is induced by the free semicategory monad on directed graphs and that the property of being strongly cartesian is preserved. As a consequence we can construct a category of arities from a category inspired by weak identity coherences, namely the category of alternatingly marked linear graphs, and show that ∆ has a special orthogonal factorisation system.

Theorem 2. The category of arities of the free relative semicategory monad f+ is isomorphic to ∆0. Thus, ∆ can be recovered as the category of free algebras of f+ over ∆0, and it admits an active/inert factorisation system (∆a, ∆0).

This active/inert factorisation system allows us to more easily express the Segal condition of [9, Section 4.3]. Additionally, using ( ∆a, ∆0), we can relate ∆ to Berger’s theory of moment categories [2]:

Theorem 3. The category ∆ has the structure of strongly unital hypermoment category.

This is joint work with Tom de Jong, Nicolai Kraus, and Simona Paoli.


12:30–13:40 70 minute lunch break

descent
13:40–14:00 Lucy Grossman: pretorsion theories on quasi-catégories.

In the 1960s, Spencer Dickson, axiomatizing properties of the category of abelian groups, presented a notion of torsion theory on abelian categories, which was soon generalized beyond the abelian setting, and even, recently, to general (and not necessarily pointed) 1−categories. Classically, a pretorsion theory on a category C is a pair of full replete subcategories (T, F) such that every morphism between them factors through their intersection, Z := T ∩ F, and that there is a notion of short exact sequence consisting of a Z−kernel and a Z−cokernel that one may associate to every object in C. Pretorsion theories satisfy multitudinous properties, including that T, F and Z are closed under certain extensions, that Z−kernels and -co-kernels are respectively monomorphisms and epimorphisms, and that T and F are respectively coreflective and reflective subcategories of C. In this presentation, we will introduce a paradigm for pretorsion theories for quasi-cat´egories, and consider some of their properties in relation to those of 1−categorical pretorsion theories, noting that many but not all of them hold. Critically, however, after passing to the homotopy category of any quasicategory equipped with one of our pretorsion theories, we obtain a one-categorical pretorsion theory. Through looking towards examples and almost-examples, we will also suggest some other generalizations of pretorsion theories in myriad directions.

14:00–14:20 Rui Prezado: lax comma categories; descent and exponentiability.

Janelidze’s categorical Galois theory provides a unifying perspective on various Galois-type theorems, which include, for instance, Magid’s Galois theory for commuta- tive rings, and Grothendieck’s Galois theory for ´etale coverings of schemes. In fact, such results were generalized and found applications in other settings.

Aiming to develop a bidimensional counterpart of Janelidze’s Galois theory, Clementino and Lucatelli Nunes initiated their research by establishing the core concepts of categorical Galois for lax comma 2-categories, which are the 2-dimensional analogue of comma categories. As these 2-categories play an important role, it then became apparent that their systematic study would provide some guiding principles in the development of such a higher dimensional notion of Galois theory.

We will give an overview our results as well as ongoing work on various sorts of lax comma categories, of both a categorical and topological flavor. More specifically, we will discuss the effective descent morphisms and exponentiable objects in these classes of (2-)categories.

This talk is based on joint work with Maria Manuel Clementino, Dirk Hofmann and Fernando Lucatelli Nunes.

14:20–14:40 Fernando Lucatelli Nunes: the semantic lax descent factorization of a functor.

In the classical context: assuming that C has pullbacks, if A : Cop → Cat is an indexed category, the descent category DescA(p) is the category of actions of the internal groupoid/equivalence induced by the kernel pair of p. The celebrated Bénabou-Roubaud Theorem shows that DescA(p) is equivalent to the category of algebras induced by A(p)! ⊣ A(p) in the classical context, under the so-called Beck-Chevalley condition.

We started investigating whether commuting properties of higher dimensional limits are useful in proving classical and new theorems of Grothendieck descent theory. Exploiting this perspective, we were able to give a generalization of the Bénabou-Roubaud Theorem in terms of commuting properties of bilimits. More than that, further investigation of commuting properties yields, in particular, to the main result of [3] which can be seen as a counterpart to the Bénabou-Roubaud Theorem, giving a characterization of monadic functors in terms of an exact condition, and showing that descent data generalizes both “algebraic structure and coalgebraic structure”, as we explain below.

Every functor that has a left adjoint has two well-known factorizations. The first one is through the category of Eilenberg-Moore algebras of the induced monad, while the second one is the factorization through the category of free coalgebras (co-Kelsili category) of the induced comonad. As usual in category theory, we also have the dual cases: a functor that has a right adjoint has a factorization through the category of Eilenberg-Moore coalgebras of the induced comonad, and other factorization through the Kleisli category of the induced monad.

We first observe that, given a 2-category A satisfying suitable hypothesis, every morphism inside a 2-category with opcomma objects (and pushouts) has a 2-dimensional cokernel diagram which, in the presence of the descent objects, induces a factorization of the morphism – that we called therein “the semantic lax descent factorization of p”. Intuitively, this is a two-dimensional (lax) version/categorification of the usual factorization of a morphism coming from the equalizer of its cokernel diagram (the (co)image factorization in case of the category of sets Set).

Our main results of this work shows that the semantic lax descent factorization of a morphism p generalizes the usual (co)Eilenberg-Moore and Kleisli factorizations. More precisely, whenever “the semantic lax descent factorization of p” coincides with the (co)Eilenberg-Moore factorization whenever p has a (right) left adjoint (or even in more lenient hypotheses).

The result is novel even in the case A = Cat, the usual 2-categories of categories. In this case, we have that every functor has a factorization through the category of descent data of its 2-dimensional cokernel diagram. We show that, if a functor F has a left adjoint, this descent factorization coincides with the factorization through the category of algebras. Dually, if F has a right adjoint, this descent factorization coincides with the factorization through the category of coalgebras. This specializes in a new connection between monadicity and descent theory. It also leads in particular to a (formal) monadicity theorem. In this talk, we present some aspects of this work in descent theory and, if time allows, we talk about ongoing work.


14:40–15:00 20 minute coffee break

causality
15:00–15:20 Dhurim Cakiqi: algorithmic syntactic causal identification.

Causal identification in causal Bayes nets (CBNs) is an important tool in causal inference allowing the derivation of interventional distributions from observational distributions where this is possible in principle. However, most existing formulations of causal identification using techniques such as d-separation and do-calculus are expressed within the mathematical language of classical probability theory on CBNs. However, there are many causal settings where probability theory and hence current causal identification techniques are inapplicable such as relational databases, dataflow programs such as hardware description languages, distrib-uted systems and most modern machine learning algorithms. We show that this restriction can be lifted by replacing the use of classical probability theory with the alternative axiomatic foundation of symmetric monoidal categories. In this alternative axiomatization, we show how an unambiguous and clean distinction can be drawn between the general syntax of causal models and any specific semantic implementation of that causal model. This allows a purely syntactic algorithmic description of general causal identification by a translation of recent formulations of the general ID algorithm through fixing. Our description is given entirely in terms of the non-parametric ADMG structure specifying a causal model and the algebraic signature of the corresponding monoidal category, to which a sequence of manipulations is then applied so as to arrive at a modified monoidal category in which the desired, purely syntactic interventional causal model, is obtained. We use this idea to derive purely syntactic analogues of classical back-door and front-door causal adjustment, and illustrate an application to a more complex causal model.

15:20–15:40 Nesta van der Schaaf: causal coverage in ordered locales.

In this talk we discuss ongoing work on causal coverages defined in ordered locales, introduced in the author’s PhD thesis. Informally, we say a region A covers U from the past if: “all information reaching U along causal paths has to have come from A.” This is supposed to generalise the canonical (Grothendieck) coverage of a locale that takes additional causal structure into account. This work is deeply inspired by a similar notion of coverage first introduced in (J. D. Christensen and L. Crane. “Causal sites as quantum geometry). Our framework provides an improvement in that the new notion of causal coverage satisfies a suitable pullback stability axiom, as expected of a coverage, whereas theirs does not. Indeed, when made precise, the above informal idea leads to a coverage relation that satisfies properties closely resembling the axioms of a Grothendieck topology: identity, pullback stability, and local characteristic.

Our motivation stems from considerations on the mathematical foundations of spacetimes. Towards applications, we will show how causal cover- ages naturally give rise to an abstract notion of domain of dependence, an import- ant concept in mathematical relativity theory. Towards abstraction, we will sketch how causal coverages can be seen as a generalised notion of Grothendieck topo- logy “taking values in a monad.” The sheaf condition with respect to causal coverages then encodes a type of deterministic evolution. An explicit example is the sheaf of solutions to the wave equation on Minkowski space.

15:40–16:00 David Ellerman: a fundamental duality in the mathematical and natural sciences: from logic to biology.

This is an essay in what might be called ``mathematical metaphysics.'' There is a fundamental duality that run through mathematics and the natural sciences. The duality starts as the logical level; it is represented by the Boolean logic of subsets and the logic of partitions since subsets and partitions are category-theoretic dual concepts. In more basic terms, it starts with the duality between the elements (Its) of subsets and the distinctions (Dits, i.e., ordered pairs of elements in different blocks) of a partition. Mathematically, the Its & Dits duality is fully developed in category theory as the reverse-the-arrows duality. The quantitative versions of subsets and partitions are developed as probability theory and information theory (based on logical entropy). Classical physics was based on a view of reality as definite all the way down. In contrast, quantum physics embodies (objective) indefiniteness. And finally, there are the two fundamental dual mechanisms at work in biology, the selectionist mechanism and the generative mechanism, two mechanisms that embody the fundamental duality.