Friday
14:00–14:20 Opening
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.
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.
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.
In this talk we will discuss various equivalent conditions for lax idempotency of a pseudomonad.
I will look at the special case of finding distributive laws for monads over themselves.
(co)monads
14:20–14:40 Quentin Aristotle: monotone weak distributive laws over the lifted powers monad in categories of algebras.
14:40–15:00 Soichiro Fujii: monad theory through enrichment.
15:00–15:20 Colin Riba: finitely accessible arboreal adjunctions and Hintikka formulae.
Joint work with Luca Reggio.
15:20–15:40 Miloslav Štěpán: some characterizations of lax idempotency for pseudomonads.
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.
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
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.
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.
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.
Probability theory is a quantitative theory.
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?
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.
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.
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.
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:
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.
11:30–11:50 Paul Blain Levy: strictifying monoidal structure, revisited.
11:50–12:10 Tomas Perutka: generalized Fox’s Theorem and pseudocommutativity.
12:10–12:30 Noam Zeilberger: context-free grammars and finite-state automata over categories.
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.
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.
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.
15:30–15:50 Henning Basold: towards formal, enriched and homotopical coalgebra.
15:50–16:00 10 minute coffee break
categorical logic
16:00–16:20 Lingyuan Ye: incompleteness and intentionality via universal property of arithmetic.
16:20–16:40 Julia Morin: Joyal’s representation theorem for Heyting categories.
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.
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
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 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.
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.
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.
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.
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.
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.
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.
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.
11:30–11:50 Mark Williams: presentations of topological modalities in homotopy type theory.
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.
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.
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.
14:00–14:20 Rui Prezado: lax comma categories; descent and exponentiability.
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.
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.
15:20–15:40 Nesta van der Schaaf: causal coverage in ordered locales.
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.