PSSL 101 - Abstracts

The abstracts below are listed in alphabetical order of the name of the author. Click here to return to the main PSSL web page.

Every accessible set functor has both a codensity monad and a density comonad. For the latter the converse also holds: the existence of a density comonad implies accessibility. In contrast, many non-accessible set functors have a codensity monad, e.g., the codensity monad of the power-set functor P assigns to a set X the set of all non-expanding self-maps of PX.

Benno van den Berg - Univalent polymorphism

This work-in-progress talk will be concerned with Hyland’s effective topos. It turns out that this topos is the homotopy category of an interesting path category (a path category is essentially a category of fibrant objects in the sense of Brown in which every object is cofibrant). Within this path category one can identify an interesting subclass of the fibrations: the discrete ones. This subclass contains a universal element, which is, however, not univalent. By passing to a more complicated category, one can obtain a universe for discrete hsets which is univalent.

Ingo Blechschmidt - Using the internal language of toposes in commutative algebra

Any commutative ring possesses a mirror image in the topos of sheaves over its spectrum, the so-called „structure sheaf“. Using the internal language of toposes, it's possible to speak about this sheaf using a naive element-based language, just as if it was a plain (non-sheafy) ring. This internal world comes with a surprise: From the internal point of view, the structure sheaf is a Noetherian ring and furthermore a field if the ring is reduced. This observation can be used to derive a new, simple, and constructive proof of Grothendieck's generic freeness lemma, a basic lemma in algebraic geometry. The talk doesn't require any prior knowledge of the internal language of toposes or of Grothendieck's generic freeness lemma.

John Bourke - Equipping weak equivalences with algebraic structure

The fibrations and trival fibrations in a model category satisfying minor size conditions can be equipped with algebraic structure.  Using Garner’s modification of Quillen’s small object argument we know that, in such a setting, there is a monad T such that a morphism bears T-algebra structure just when it is a fibration; similarly for the trivial fibrations.

What about the weak equivalences?  It turns out that a lot can be said.  We will see, for instance, that there is a monad T such that a morphism of topological spaces bears T-algebra structure just when it is a weak homotopy equivalence.  Similarly for quasi-isomorphisms and many other kinds of weak equivalence.  Furthermore, we will give a complete description of the extent to which the weak equivalences in a combinatorial model category can be equipped with algebraic structure.

Andrew Brooke-Taylor - Powerful Images for Abstract Elementary Classes

Abstract elementary classes (AECs) and accessible categories can be viewed as two approaches to model theory going beyond the first order setting, and whilst they were developed completely independently of each other, they turn out to be closely related.  After reviewing the basics of this connection, I will talk about joint work with Rosicky, in which we used the accessible categories perspective to improve an important result about AECs, reducing the large cardinal axiom used down to the optimal assumption.  Specifically, we reduced the large cardinal axiom used to show that the powerful image of any accessible functor is accessible; thanks to prior results of Lieberman and Rosicky, this shows that under the same large cardinal assumption, every AEC is tame.

Georgios Charalambous - On Galois and Tannakian categories

Several attempts have been made to unify the theories of Galois and Tannakian categories. However the theories remain essentially independent until now. In this talk we will explain in what sense they are not, and how they are in fact very naturally related

Alexander Corner - Fubini for codescent objects

I will introduce a 2-dimensional analogue of extranatural transformation and use it to characterise codescent objects. They will be seen as universal objects amongst extrapseudonatural transformations in a similar manner in which coends are universal objects amongst extranatural transformations. A Fubini theorem for codescent objects will be then be discussed. I will go on to mention the use of this characterisation in describing Day convolution for monoidal bicategories.

Ivan Di Liberti  - Weak saturation and weak amalgamation property

The two model-theoretic concepts of weak saturation and weak amalgamation property are studied in the context of accessible categories. We relate these two concepts providing sufficient conditions for existence and uniqueness of weakly saturated objects of an accessible category $K$. We discuss the implications of this fact in classical model theory.

Christian Espindola - Stone duality for infinitary first-order logic

Makkai's reconstruction result allows to recover a first-order theory, up to pretopos completion, from its category of models by equipping it with appropriate structure and considering set-valued functors preserving this structure. One of the difficulties in extending this result to the infinitary case is that the Keisler-Shelah isomorphism theorem, which asserts that elementarily equivalent models have isomorphic ultrapowers, does not hold for infinitary logic. However, we will see that the theory of accessible categories can provide extra structure, under appropriate large cardinal assumptions, to recover the theory from its category of models up to a notion of infinitary pretopos-completion. More precisely, the plan of Makkai of endowing the categories of models with extra structure coming from ultraproducts can be readily generalized to the infinitary case in the presence of a compact cardinal, by means of which an infinitary version of Los theorem is possible. Makkai's use of Keisler-Shelah theorem allows him to regulate the behaviour of subfunctors of set-valued functors from the category of models, while the use of Vopenka's principle in our case, in the form "every subfunctor of an accessible functor is accessible" will provide the desired effect. For the reconstruction result, one more large cardinal axiom needs to be assumed, namely that the class of ordinals Ord is weakly compact. With these assumptions, a duality theory arises for the infinitary case that generalizes the one exposed by Makkai.

Eric Faber - Toposes of  finitely supported M-Sets

I will introduce toposes of  nitely supported M-Sets, where M is a monoid of endomorphisms of some  rst-order structure. The study of this particular class of toposes is motivated by a host of examples, such as nominal sets, cubical sets and simplicial sets. For cubical sets, this presentation and the connection to nominal sets originates from work by Andrew Pitts. In my talk I will sketch a preliminary characterization of such toposes, suggesting connections with (geometric) model theory and work by Makkai on duality for Boolean pretoposes.

Enrico Ghiorzi - Internal enriched categories

I will propose a definition of internal enriched categories, which internalizes the standard notion of enrichment. Within my definition, internal enriched categories are related to Shulman’s enriched indexed categories and Leinster’s V-enriched T-multicategories. I will recall these notions and show how they relate to internal enriched categories.

Julia Goedecke - Hopf formulae for Tor

A Hopf formula expresses a homology object in terms of a projective presentation, its kernel and certain (generalised) commutators.  The first such formula, for second group homology, was given by Hopf in 1942.  Over the last 13 years or so, Everaert, Gran, Van der Linden and others have developed Hopf formulae in more general categorical contexts.  One of these general contexts is that of a semi-abelian category with a Birkhoff subcategory where the reflector factors through a protoadditive functor.  In that generality, some elements of the Hopf formula are necessarily very abstract. With Tim Van der Linden and Guram Donadze, I am studying the special situation of subvarieties of categories of $$R$$-modules. It can be seen using properties of algebraic theories that every such subvariety is again a category of modules. Here we can find explicit and easy formulations of the generalised commutators. Since the reflector in this situation turns out to be tensoring, the resulting homology functors are Tor functors.  Through these fairly simple formulations we obtain new ways of calculating, for example, homology of Lie algebras, and Hochschild homology of an associative unital algebra. More generally, our results apply to any abelian Birkhoff subcategory of any semi-abelian variety, using a factorisation through the abelian core.

Sina Hazratpour - Fibrations of Toposes

The notions of (op)fibration in the 2-category of toposes and geometric morphisms have close connections with topological properties. For example, every local homeomorphism is an opfibration. This connection is in line with the conception of toposes as generalized spaces.   Although Johnstone’s definition of (op)fibrations in 2-categories in the Elephant is well-suited for working in the 2-category of bounded toposes, it is rather complicated and difficult to work with in practice.   I shall describe how a simpler definition can be given in Vickers's 2-category of contexts for arithmetic universes based on prior work of R.Street. This will give rise to (op)fibrations of toposes as in the Elephant definition, and it can be used to prove some of the topos results.

Peter Hines - A diagrammatic calculus for cryptographic protocols

This talk introduces a method of representing cryptographic protocols as categorical diagrams. A single diagram is used to model the algebraic information, epistemic knowledge, and information flow, together with their interaction. This is illustrated using several examples of commonly used protocols.

A 'correctness criterion' for protocols is introduced, based on a 2-categorical interpretation of such diagrams, and the examples presented are shown to satisfy this criterion.  Theoretical justifications for this correctness criterion are given, along with illustrations of the security flaws that arise when this criterion is not satisfied.

Algorithmic applications are discussed, based on the notion of 'completing' a partially specified protocol to one that satisfies the correctness criterion. If time permits, connections between cryptography, cryptanalysis, and the foundations of categorical coherence will also be explored.

Peter Johnstone - Anti-Boolean toposes and infinitesimal generation

Mat\'ias Menni has recently observed that every sufficiently cohesive topos is what he calls infinitesimally generated', in the sense that there is a small' object (one having a \neg\neg-dense point) which does not belong to any proper sheaf subtopos. We show that this is actually a fairly common property; it holds in any topos which is anti-Boolean' in the sense that its only open Boolean subtopos is degenerate.

Jürgen Koslowski - Augmenting graphs with memory:  categorical models for (2)PDAs and generalised context-free grammars

We wish to extend the description of finite automata (FAs) via labeled transition systems (LTSs) to push-down automata (PDAs) and 2PDAs (the latter are equivalent to Turing machines). Note that a similar description of context-free grammars (CFGs) is a consequence of Bob Walters' work on context-free languages (1989). Here the reflexive(!) graphs underlying traditional LTSs are replaced by reflexive (co-)multigraphs, and the free monoid over a set A is replaced by the free (co-) multicategory, which has rooted planar trees with nodes labeled in A or the empty word as morphisms.

Both approaches can be combined to yield a notion of `transition-controlled grammar'', where memory is introduced in the form of vertical morphisms, to avoid interference with the horizontal transitions.  Hence our models take the form of double categories, or at least computads for those.  Restricting the trees to left-sided trees (corresponding to left derivations in grammars) and explicitly making parallel tree composition partial, results in PDAs, as desired. 2PDAs require cospans of memory.

Of particular interest is the construction of the codomain of these generalised transition systems out of the free categories over some  finite graph (for the transitions), and the free (co-)multicategory of A-labeled trees, as it utilises the Gray tensor product.

Nicolai Kraus - (n,1)-Categories in Univalent Type Theory

I present an approach to univalent (n,1)-categories in type theory.  This definition of higher categories tries to mimic the usual definition of Segal spaces, replacing simplicial sets by types.  The difficult part is adding the identities to the construction, since the usual Reedy-style encoding of type-valued diagrams over the simplex category ("semisimplicial types") does not include degeneracies.  This is remedied with the help of a trick suggested by Lurie and Harpaz.  I show that the special case n=1 leads to a definition which is equivalent to the univalent categories of Ahrens-Kapulkin-Shulman.  The talk is based on arXiv:1707.03693 (joint work with Paolo Capriotti).

Vaia Patta - A categorical perspective on Entropy and a categorification of topological semimodules

Starting out from Lieb and Yngvason’s axiomatization of Entropy in terms of a preorder, we embellish their framework to retrieve a description of distinct classes of adiabatic processes (labelled by a nonthermodynamical property such as duration). To that end, we categorify topological semimodules to get topological “weak” semimodules, which appear to be versatile enough to describe common mathematical constructions (one example being Kronecker products and powers). There is an adjunction between LY’-categories (that is, a straightforward generalisation of Lieb and Yngvason’s model) and the more general topological “weak semimodules”, which gives rise to an idempotent comonad. Lastly, certain LY’-categories over the nonnegative real numbers are traced monoidal; this includes physically relevant categories that describe thermodynamic states and adiabatic processes.

Jiří Rosický  -  Internal sizes in accessible categories

The internal size of an object M inside a given category is, roughly, the least infinite cardinal $\lambda$ such that any morphism from M into the colimit of a $\lambda^+$-directed system factors through one of the components of the system. The existence spectrum of a category is the class of cardinals $\lambda$ such that the category has an object of internal size $\lambda$. We study the existence spectrum in μ-abstract elementary classes ($\mu$-AECs), which are, up to equivalence of categories, the same as accessible categories with all morphisms monomorphisms. We show for example that, assuming instances of the singular cardinal hypothesis which follow from a large cardinal axiom, $\mu$-AECs which admit intersections have objects of all sufficiently large internal sizes. We also investigate the relationship between internal sizes and cardinalities and analyze a series of examples, including one of Shelah---a certain class of sufficiently-closed constructible models of set theory---which show that the categoricity spectrum can behave very differently depending on whether we look at categoricity in cardinalities or in internal sizes. This talk is based on a joint work with M. Lieberman and S. Vasey.

Jiří Rosický  -  Barely locally presentable categories

We introduce a new class of categories generalizing locally presentable ones. The distinction does not manifest in the abelian case and, assuming Vopěnka's principle, the same happens in the regular case. Under the negation of this principle, there are barely locally presentable categories which are not locally presentable. The natural example is the dual of a  certain category of proximity spaces. Without set theory, we do not know any barely locally presentable category which is not locally presentable.  This talk is based on a joint work with L. Positselski.

Andrew Swan - Lifting Problems in a Grothendieck Fibration

The notion of lifting problem is an important concept both in homotopical algebra and the semantics of homotopy type theory. Often when working with lifting problems it’s useful to have some notion of family of maps. A simple example is that a map f has the right lifting property against a set indexed family of maps (m_i)_{i \in I} if for each i in I, each lifting problem of m_i against f has a filler. In a more sophisticated notion due to Garner, the set indexed family of maps can be replaced with a functor from a small category to the arrow category. When working with realizability variants of cubical sets, it’s useful to have other notions of family of maps. I’ll give a general notion of lifting problem that applies in any Grothendieck fibration and show how to recover Garner’s definition by applying it to the fibration of “category indexed families.” Applying the general definition to codomain fibrations yields many interesting examples and helps us to understand better a notion of lifting problem internal to a topos studied by various authors including Stekelenburg, Coquand, Pitts and Orton, Van den Berg and Frumin. A version of the small object argument applies to codomain functors over toposes with natural number object and satisfying the axiom of weakly initial set of covers (WISC), which gives some interesting examples of algebraic weak factorisation systems.

Adjunctions that agree with both their Eilenberg--Moore completion and its dual have arisen in several settings but the extension to them of textbook results about monads seems to have been rather fragmentary.   I would like some hints on both applications and potential results. My applications are (1) Steve Vickers' notion of colocale or localic locale, which is a coalgebra for the adjunction of frames over dcpos and (2) adding abstract Stone duality to Nick Benton and Gavin Bierman's linear-non-linear models, which combined Girard's "of course" with Moggi's computational monads. My results so far include (1) EM bi-completions, (2) lifting colimits, (3) lifting products and their relationship to tensor products of algebras, (4) KZ (ordered) monads, (5) Beck distributivity.

Christopher Townsend - Hilsum-Skandalis maps in a cartesian category

Hilsum-Skandalis maps, from differential geometry, are the 'right' morphisms between differential groupoids. The talk will outline how the theory of Hilsum-Skandalis maps can be developed relative to an arbitrary cartesian category and show how in this context Hilsum-Skandalis maps can be represented as certain adjunctions that stably satisfy Frobenius reciprocity. I will describe how this representation (i) eases results about Hilsum-Skandalis maps, (ii) can be used to recover basic results about geometric morphisms; and, (iii) suggests a theory of continuous maps more general than geometric morphisms.

Dominic Verdon - Coherence for symmetric and braided pseudomonoids

We prove coherence results for naked, braided and symmetric pseudomonoids in naked, braided and symmetric semistrict monoidal bicategories (Gray monoids) using movies of string diagrams. These theorems generalise MacLane's coherence theorems for braided and symmetric monoidal categories to arbitrary braided and symmetric pseudomonoids. Through doing this we develop a toolkit and language that can be used to investigate other algebraic theories in the higher braided/symmetric setting

Dominic Verity - Generator notions in $\infty$-cosmology

∞-Cosmoi provide a framework in which to develop the abstract category theory of various kinds of (∞, 1)-categorical structures. In essence, an ∞-cosmos is simply a  finitely complete (∞, 2)-category, although for expository reasons they are often taken to be categories of  fibrant objects enriched in the Joyal model structure. This notion is general enough to immediately encompass most of the common models of (∞, 1)-categories; quasi-categories, complete Segal-spaces, Θ1-spaces and suchlike. At the same time, it is powerful enough to develop a theory of (co)cartesian fibrations, a calculus of two-sided modules (pro-functors), Yoneda’s lemma, theories of adjunction and Kan extension and so forth. Indeed, much of this theory can be developed in the setting of the (strict, classical) homotopy 2-category obtained from the ∞-cosmos by applying the homotopy category construction to its hom-spaces. In this talk we briefy recap the cosmological approach to the category theory of ∞-categorical structures and discuss how it encompasses  bred categorical notions. This leads us naturally to the study of certain generating sets of “compact” objects in an ∞-cosmos, a mechanism which allows us to adapt certain  brewise arguments into the ∞-cosmos framework. Joint work with Emily Riehl.

Jonathan Weinberger - Interpreting type theory in appropriate presheaf toposes

In [CCHM16] Coquand et al. have presented a model for a variant of Martin-Löf type theory called Cubical Type Theory (CTT) which allows one to prove Voevodsky's Univalence Axiom and establish the existence of various Higher Inductive Types. The model they describe lives within a presheaf topos of so-called cubical sets.

The aim of this talk is to reformulate this model in more categorical terms using the internal language of the ambient topos as much as possible. In this respect our approach is inspired by [OP16] where they work within an anonymous topos. We restrict to presheaf toposes since they allow
for an explicit construction of a universe as opposed to loc. cit. where a universe is just postulated. This allows us to perform the so-called glueing construction as in [CCHM16] without postulating an ad hoc condition on the universe as in [OP16].

In [CCHM16] the authors have given an interpretation of CTT in a presheaf topos $\widehat{\C} = \Set^{\C^\op}$ where $\C$ is the opposite of the category of finitely presented free de Morgan algebras. Though we will consider this particular site as a running example, we want to keep a certain level of generality in our exposition with the intention of identifying a minimal set of assumptions on  $\C$ sufficient for obtaining a model of CTT.

In [CCHM16] they have described their model externally without making use of the internal language of the topos $\widehat{\C}$ as opposed to [OP16]. We prefer this latter version because it allows one to formulate things more concisely. But for this purpose we need a universe in $\widehat{\C}$ which can be constructed à la Hofmann and Streicher [Str05]. As is well known, $\widehat{\C}$ gives rise to a model of extensional type theory with a proof irrelevant impredicative universe as given by the subject classifier $\Omega$ where equivalent propositions are already equal.

We also adapt the notion of a glueing construction, as considered in [CCHM16, OP16], to our generalized sites. As in [CCHM16] this glueing construction is crucial for showing that the universe of fibrant types validates Voevodsky's univalence axiom.

Though not checked in every detail, we think that Gambino and Sattler's approach [GS17, Sat17] based on algebraic model structures may be considered as an externalization via Kripke-Joyal semantics of the respective internal definitions employed in [OP16] and our work.

Finally, we argue that the cubical set model construction can be carried out as well in categories of internal presheaves $\mathcal E^{\mathcal C}$ for certain categories $\mathcal E$ modelling extensional type theory with universes, where $\mathcal C$ denotes the category of finitely presented free de Morgan algebras internal to $\mathcal E$. In particular we can instantiate $\mathcal E$ by the category of assemblies for a given partial combinatorial algebra, so as to obtain realizability models for CTT with impredicative universe (cf. recent work by Awodey, Frey and Hofstra [Awo17, Fre17]).

References:

[Awo17] S. Awodey (2017)  Impredicative Encodings in HoTT (or: Toward a Realizability $\infty$-Topos) Big Proof, Cambridge, 11 July 2017, Slides

[BBCGSV16] L. Birkedal, A. Bizjak, R. Clouston, H.B. Grathwohl, B. Spitters, A. Vezzosi (2016) Guarded Cubical Type Theory Preprint, arXiv:1611.09263

[CCHM16] T. Coquand, C. Cohen, S. Huber, A. Mörtberg (2016) Cubical Type Theory: a constructive interpretation of the univalence axiom.  To appear in postproc. of TYPES 2015, arXiv:1611.02108

[Fre17] J. Frey (2017) Towards a realizability model of homotopy type theory, CT 2017, Vancouver, 21 July 2017, Slides

[GS17] N. Gambino, C. Sattler (2017), The Equivalence Extension Property and Model Structures, Accepted for pub. in J. Pure Appl. Algebr., arXiv:1510.00669

[Sat17] C. Sattler (2017) The Equivalence Extension Property and Model Structures. Preprint arXiv:1704.06911

[OP16] I. Orton, A.M. Pitts (2016) Axioms for Modelling Cubical Type Theory in a Topos. CSL 2016, 62 (24). doi:0.4230/LIPIcs.CSL2016.24

[Str05] T. Streicher (2005) Universes in Toposes. From Sets and Types to Topology and Analysis: Towards practicable foundations for constructive mathematics 48, 78