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

Jiří
Adámek - *Codensity monads and density comonads of set functors*

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 -

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 -

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 -

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 -

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 -

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 -

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 -

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 -

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 -

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 -

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 -

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 -

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 -

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ý -

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 -

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.

Paul Taylor - *Bimonoidal
adjunctions*

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 -

∞-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 -

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

Click here to return to the main PSSL web page.

Last modified on September 8th, 2017 by Nicola Gambino.