Categorical Algebra and Computation

A Workshop in Honour of John Power on the occasion of his 60th Birthday

23rd December 2019

Room 420, Research Institute for Mathematical Sciences, Kyoto University


10:00-10:15 Opening / Introduction (Masahito Hasegawa)
Session 1 (Chair: Shin-ya Katsumata)
10:15-10:45 Yuichi Komorida (National Institute of Informatics)
Injective objects and fibered codensity liftings
10:45-11:20 Soichiro Fujii (Kyoto University)
Hom weak n-categories of a weak (n+1)-category
11:20-11:45 Break
Session 2 (Chair: Ichiro Hasuo)
11:45-12:15 Ken Sakayori (University of Tokyo)
Compact closed Freyd category and π-calculus
12:15-12:45 Shin-ya Katsumata (National Institute of Informatics)
A double category theoretic analysis of graded linear exponential comonads
12:45-14:00 Lunch @ Room 110 (ground floor)
Session 3 (Chair: Soichiro Fujii)
14:00-14:45 Steve Lack (Macquarie University)
Weak adjoint functor theorems
14:45-15:30 Coffee & Cake @ Room 110
Session 4 (Chair: Makoto Takeyama)
15:30-16:00 Yoshiki Kinoshita (Kanagawa University)
16:00-16:45 John Power (Macquarie University)
Lawvere theories and finitary monads: an enriched approach
16:45- Closing
18:00- Dinner @ OMEN

Abstracts and Slides

Introduction by Masahito Hasegawa

[ Slides ]

Yuichi Komorida : Injective objects and fibered codensity liftings

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 ]

Soichiro Fujii : Hom weak n-categories of a weak (n+1)-category

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 John Power.

[ Slides ]

Ken Sakayori : Compact closed Freyd category and π-calculus

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 ]

Shin-ya Katsumata : A double category theoretic analysis of graded linear exponential comonads

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 2018.

Steve Lack : Weak adjoint functor theorems

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 ]

Yoshiki Kinoshita : Hiza-gawari

John Power : Lawvere theories and finitary monads: an enriched approach

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)

[ Page Top | Workshop Page ] Last modified: 23 December 2019