Related papers: Doctrines, modalities and comonads

Deduction is the one of the major forms of inferences and commonly used in formal logic. This kind of inference has the feature of monotonicity, which can be problematic. There are different types of inferences that are not monotonic, e.g.…

We define a notion of grading of a monoid T in a monoidal category C, relative to a class of morphisms M (which provide a notion of M-subobject). We show that, under reasonable conditions (including that M forms a factorization system),…

We provide a co-free construction which adds elementary structure to a primary doctrine. We show that the construction preserves comprehensions and all the logical operations which are in the starting doctrine, in the sense that it maps a…

In recent years we have seen several new models of dependent type theory extended with some form of modal necessity operator, including nominal type theory, guarded and clocked type theory, and spatial and cohesive type theory. In this…

Many complex tasks can be decomposed into simpler, independent parts. Discovering such underlying compositional structure has the potential to enable compositional generalization. Despite progress, our most powerful systems struggle to…

Lenses may be characterised as objects in the category of algebras over a monad, however they are often understood instead as morphisms, which propagate updates between systems. Working internally to a category with pullbacks, we define…

We start from two closure operators defined on the elements of a special kind of partially ordered sets, called causal nets. Causal nets are used to model histories of concurrent processes, recording occurrences of local states and of…

We define a monad $T_n^{\operatorname{D^s}}$ whose operations are encoded by simple string diagrams and we define $n$-sesquicategories as algebras over this monad. This monad encodes the compositional structure of $n$-dimensional string…

Categories can be identified -- up to isomorphism -- with polynomial comonads on Set. The left Kan extension of a functor along itself is always a comonad -- called the density comonad -- so it defines a category when its carrier is…

A double category is constructed from a `fattened' version of a given category, motivated in part by a context of parallel transport. We also study monoidal structures on the underlying category and on the fattened category.

We describe how self-adjoint ordered operator spaces, also called non-unital operator systems in the literature, can be understood as $*$-vector spaces equipped with a matrix gauge structure. We explain how this perspective has several…

Motivated by an ongoing project on computer aided derivation of asymptotic models governed by partial differential equations, we introduce a class of term transformations that consists of traversal strategies and insertion of contexts. We…

The laws of physics have been written in the language of dif-ferential equations for centuries. Neural Ordinary Differen-tial Equations (NODEs) are a new machine learning architecture which allows these differential equations to be learned…

TheBench is a tool to study monadic structures in natural language. It is for writing monadic grammars to explore analyses, compare diverse languages through their categories, and to train models of grammar from form-meaning pairs where…

Calculi of string diagrams are increasingly used to present the syntax and algebraic structure of various families of circuits, including signal flow graphs, electrical circuits and quantum processes. In many such approaches, the semantic…

This paper investigates some issues arising in categorical models of reversible logic and computation. Our claim is that the structural (coherence) isomorphisms of these categorical models, although generally overlooked, have decidedly…

In the present work, a natural sequel to \cite{MaPi1}, we further discuss the existence of adjunctions between categories of institutions and of $\pi$-institutions. This is done at both a foundational and an applied level. Firstly, we…

We study Boolean classification problems over relational background structures in the logical framework introduced by Grohe and Tur\'an (TOCS 2004). It is known (Grohe and Ritzert, LICS 2017) that classifiers definable in first-order logic…

We display a family of Stone-type dualities linking categories of frames carrying pairs of modal operators to categories of spaces carrying a binary relation. Different notions of morphism used on the relational side lead to significant…

This paper describes a method for compiling a constraint-based grammar into a potentially more efficient form for processing. This method takes dependent disjunctions within a constraint formula and factors them into non-interacting groups…