Abstracts and Slides
Introduction by Masahito Hasegawa
[ Slides ]
Functor lifting along a fibration is used in several scenes in computer science. In the theory of coalgebras,
it is used to define coinductive predicates. Codensity lifting is a scheme to obtain a lifting of an endofunctor
along a fibration. It generalizes a few previous lifting schemes, which include Kantorovich lifting. Hinted by
a result for Kantorovich lifting, we identify a sufficient condition for a codensity lifting to be fibered.
We see that this condition applies to many examples that have been studied. As an application, we derive
some result on bisimilarity-like notions.
[ Slides ]
Weak low dimensional categories are defined inductively; for example, a bicategory has a set of objects and
hom categories, and a tricategory has a set of objects and hom bicategories. On the other hand, Leinster has
proposed a definition of weak n-category for all natural number n, based on an earlier definition by Batanin.
In Leinster’s definition, weak n-categories are defined to be Eilenberg-Moore algebras of a certain monad on
the category of n-graphs. In fact, from this definition it is not obvious that a weak (n+1)-category has a
``hom weak n-category’’ for every pair of objects. In this talk, after a brief review of Leinster’s definition,
I will explain how one can associate to each weak (n+1)-category its underlying (weak n-category)-enriched graph,
consisting of the same objects and the hom weak n-categories. This is based on joint work with Thomas Cottrell and
[ Slides ]
The notion of closed Freyd category, introduced by Power and Thielecke, provides us with an axiomatisation of models of effectful programming languages.
In this talk, we investigate a model of concurrent programming languages based on closed Freyd category.
We introduce compact closed Freyd category, a closed Freyd category whose premonoidal category is monoidal and furthermore compact closed.
The bifunctoriality of the premonoidal product means that f and g in f ⊗ g are evaluated concurrently.
Compact closed structure describes processes interconnected via ports.
We show that this categorical structure corresponds to a variant of the i/o-typed π-calculus.
This is the first categorical model of the π-calculus, to the best of our knowledge, except for session-typed variants in which only well-structured communications can be expressed.
The corresponding equational theory has a notable axiom called the η-rule, which is a necessary condition for a term model to be a category under a mild assumption.
Most of the behavioural equivalences, however, do not satisfy the η-rule and we believe this is why a categorical model of the π-calculus has not been found.
[ Slides ]
Graded linear exponential comonads are an extension of linear
exponential comonads wih grading, and provide a categorical semantics
of resource-sensitive exponential modality in linear logic. In this
paper, we propose a concise double-category theoretic formulation of
graded linear exponential comonads as a kind of monoid homomorphisms
from the multiplicative monoids of semirings to the composition
monoids of symmetric monoidal endofunctors. We also exploit this
formulation to derive the category of graded comonoid-coalgebras,
which decompose graded linear exponential comonads into symmetric
monoidal adjunctions plus twists. This work was published in FoSSaCS
The General Adjoint Functor Theorem of Freyd has a straightforward extension to the enriched setting. There is also
a Weak Adjoint Functor Theorem, due to Kainen, and providing a sufficient condition for the existence of a weak left adjoint,
where weakness refers to the existence but not uniqueness of factorizations.
I will report on recent joint work with John Bourke and Lukas Vokrinek, in which we prove a weak adjoint functor theorem in
the enriched context. This actually contains the other three theorems as special cases. Our base for enrichment will be a
monoidal model category.
Our motivating example involves simplicially enriched categories, where the base category of simplicial sets is equipped with
the Joyal model structure. The theorem then has applications to the Riehl-Verity theory of infinity-cosmoi.
[ Slides ]
We give a new account of the correspondence, developed by Lack, Nishizawa and Power, between finitary monads and Lawvere
theories over an arbitrary locally finitely presentable base. The passage from a finitary monad to the corresponding Lawvere theory
is exhibited as a free completion of an enriched category under absolute tensors, extending work of Garner, who established the result
for finitary monads and Lawvere theories over the category of sets. The generalisation inherently requires enrichment over a bicategory.
(joint with Richard Garner)