Assume-guarantee reasoning is a technique for compositional model checking in which system specifications are checked under certain assumptions on system parameters or inputs, and provide guarantees on observations of system state. We present a categorical framework for assume-guarantee reasoning for safety problems by viewing systems as lenses, following our earlier work on the compositionality of generalized Moore machines. Generalized Moore machines include ordinary Moore machines, partially observable Markov (decision) processes, and systems of parameterized ODEs (control systems); our framework gives assume-guarantee reasoning specially adapted to each of these cases. In particular, we give a novel formulation of assume-guarantee reasoning for (local) input-to-state stability ((L)ISS) Lyapunov functions on systems of parameterized ODEs.
Our framework is categorically natural and straightforwardly compositional. A flavor of generalized Moore machine is determined by a tangency: a fibration with a section. We show that symmetric monoidal loose right modules of assume-guarantee certified generalized Moore machines over symmetric monoidal double categories of certified wiring diagrams can be constructed 2-functorially from fibrations internal to the 2-category of tangencies.

Talk at the internal seminar for the ARIA 'Safeguarded AI' programme on propositional quantitative linear logic.

Follow up to A Taste of Quantitative Logic.

In this talk I introduce \(p\)-means and argue they form a good quantitative analogue of first-order quantifiers. I then sketch the construction of a hyperdoctrine valued in enriched graded preorders which forms the intended semantics of a first-order quantitative linear logic.

Quantitative logic, after Lawvere, is one whose judgments are valued in real numbers, rather than merely being a logic about real numbers. By doing so we can guarantee good structural properties of the logic, such as being able to treat addition as an additive connective in the sense of Girard. Moreover, by employing the full spectrum of sums multiplication distributes over, we are able to approximate 'hard' connectives with 'soft' ones, with application in machine learning. In the first part of the talk I will showcase these features by describing a sequent calculus for a quantitative version of linear logic.

This is work in progress with Atkey, Grellois, and Komendantskaya.

We study how discrete opfibration classifiers in a(n enhanced) 2-category can be endowed with the structure of a \(T\)-algebra and thereby lift to the enhanced 2-category of 2-algebras and lax morphisms. To support this study, we give a definition of discrete opfibration classifier in the enhanced setting in which tight (e.g. strict) discrete opfibrations are classified by loose (e.g. lax) maps.

We then single out conditions on the 2-monad \(T\) and the classifier that make this possible, and observe these hold in a wide range of examples: double categories (recovering the results of Parè and Lambert), (symmetric) monoidal categories, and all structures encoded by familial 2-monads. We also prove the properties needed on such 2-monads are stable under replacement by pseudo-algebra coclassifiers (when sufficient exactness conditions hold), allowing us to replace a pseudo-algebra structure on the classifier by a strict one.

To get to our main theorem, we introduce the concepts of cartesian maps and cartesian objects of a 2-algebra, which generalize various other notions in category theory such as cartesian monoidal categories, extensive categories, categories with descent, and more. As a corollary, we characterize when representable copresheaves are pseudo rather than lax in terms of the cartesianity at their representing object.

In this talk I report on work in progress, joint with David Jaz Myers, about lifting discrete opfibration classifiers (2-classifiers, i.e. a '\(\mathsf {Set}\)'-like object) from a 2-category \(\mathcal {K}\) to the 2-category of algebras of a 2-monad \(T\).

In the setting of DOTS, we often construct behaviour functors as 'representables', but without a 2-classifier one can't really call these 'representables'. Moreover, there is a strong connection between compositionality of such functors, the properties of the algebra they map out of, and the properties of the object(s) that represents them.

These phenomena are in fact completely general, so we set out to better understand the situation and found some frankly interesting notions and results, chiefly a tight result on the existence of 2-classifiers for 2-algebras.

We introduce contextads and the \(\mathbb {C}\mathsf {tx}\) construction, unifying various structures and constructions in category theory dealing with context and contextful arrows -- comonads and their Kleisli construction, actegories and their \(\mathcal {P}\mathsf {ara}\) construction, adequate triples and their \(\mathbb {S}\mathsf {pan}\) construction. Contextads are defined in terms of Lack-Street wreaths, suitably categorified for pseudomonads in a tricategory of spans. This abstract approach can be daunting, so in this talk we will work with a lower-dimensional version of contextads which is relevant to capture dependently graded comonads arising in functional monadic programming. In fact we show that many side-effects monads can be dually captured by discrete contextads, seen as dependently graded comonads, and gesture towards a general result on the 'transposability' of parametric right adjoint monads to dependently graded comonads.

Talk at the internal seminar for the ARIA 'Safeguarded AI' programme. A follow up of last year's preprint on quantifiers for quantitative reasoning.

The talk concerns the recent work with Baltieri, Biehl and Virgo on a categorical account of the classical 'internal model principle' from control theory and cybernetics in a broader sense. The aim is to distill the mathematical content of such an informal principle, following previous work of Wonham and Hepburn. In the talk I only use elementary mathematical notions and thus should be accessible to an audience acquainted with the basic vocabulary of sets and dynamical systems.

The internal model principle, originally proposed in the theory of control of linear systems, nowadays represents a more general class of results in control theory and cybernetics. The central claim of these results is that, under suitable assumptions, if a system (a controller) can regulate against a class of external inputs (from the environment), it is because the system contains a model of the system causing these inputs, which can be used to generate signals counteracting them. Similar claims on the role of internal models appear also in cognitive science, especially in modern Bayesian treatments of cognitive agents, often suggesting that a system (a human subject, or some other agent) models its environment to adapt against disturbances and perform goal-directed behaviour. It is however unclear whether the Bayesian internal models discussed in cognitive science bear any formal relation to the internal models invoked in standard treatments of control theory. Here, we first review the internal model principle and present a precise formulation of it using concepts inspired by categorical systems theory. This leads to a formal definition of 'model' generalising its use in the internal model principle. Although this notion of model is not a priori related to the notion of Bayesian reasoning, we show that it can be seen as a special case of possibilistic Bayesian filtering. This result is based on a recent line of work formalising, using Markov categories, a notion of 'model' generalising its use in the internal model principle. Although this notion of model is not a priori related to the notion of Bayesian reasoning, we show that it can be seen as a special case of possibilistic Bayesian filtering. This result is based on a recent line of work formalising, using Markov categories, a notion of 'interpretation', describing when a system can be interpreted as performing Bayesian filtering on an outside world in a consistent way.

Category theory has a long history of being applied to the study of general systems. Double Categorical Systems Theory (DCST) condenses many lessons learned along the way regarding compositional structures for the representation of systems, their behaviour and the interaction of these two aspects. In this talk I'll revisit old and new wisdom regarding functorial behaviour of systems represented by a category of timepieces, and prove old and new compositionality theorems for them.

We introduce contextads and the Ctx construction, unifying various structures and constructions in category theory dealing with context and contextful arrows -- comonads and their Kleisli construction, actegories and their Para construction, adequate triples and their Span construction. Contextads are defined in terms of Lack--Street wreaths, suitably categorified for pseudomonads in a tricategory of spans in a 2-category with display maps. The associated wreath product provides the Ctx construction, and by its universal property we conclude trifunctoriality. This abstract approach lets us work up to structure, and thus swiftly prove that, under very mild assumptions, a contextad equipped colaxly with a 2-algebraic structure produces a similarly structured double category of contextful arrows. We also explore the role contextads might play qua dependently graded comonads in organizing contextful computation in functional programming. We show that many side-effects monads can be dually captured by dependently graded comonads, and gesture towards a general result on the `transposability' of parametric right adjoint monads to dependently graded comonads.

We develop a categorical framework for reasoning about abstract properties of differentiation, based on the theory of fibrations. Our work encompasses the first-order fragments of several existing categorical structures for differentiation, including cartesian differential categories, generalised cartesian differential categories, tangent categories, as well as the versions of these categories axiomatising reverse derivatives. We explain uniformly and concisely the requirements expressed by these structures, using sections of suitable fibrations as unifying concept. Our perspective sheds light on their similarities and differences, as well as simplifying certain constructions from the literature.

We model problems as presheaves that assign sets of certificates to input instances, and we show how to use presheaf Čech cohomology to capture the precise ways in which local solutions fail to patch into global ones. Applied to problems like Vertex Cover, Cycle Cover, and Odd Cycle Transversal, our framework exposes emergent phenomena such as hidden cycles or the inflation of small, local solutions. This approach not only rephrases classical results like König's Theorem in cohomological terms, but also reveals how to systematically account for failures of compositionality. Although our main focus is on presheaves of sets, the methods generalize naturally to Abelian presheaves, suggesting a rich interplay between graph theory, cohomology, and complexity. This work represents a first step toward a systematic, sheaf-theoretic theory of algorithmic structure and related obstructions.

Organizing physics has been a long-standing preoccupation of applied category theory, going back at least to Lawvere. We contribute to this research thread by noticing that Hamiltonian mechanics and gradient descent depend crucially on a consistent choice of transformation -- which we call a reaction structure -- from the cotangent bundle to the tangent bundle. We then construct a compositional theory of reaction structures. Reaction-based systems offer a different perspective on composition in physics than port-Hamiltonian systems or open classical mechanics, in that reaction-based composition does not create any new constraints that must be solved for algebraically.

The technical contributions of this paper are the development of symmetric monoidal categories of open energy-driven systems and open differential equations, and a functor between them, functioning as a "functorial semantics" for reaction structures. This approach echoes what has previously been done for open games and open gradient-based learners, and in fact subsumes the latter. We then illustrate our theory by constructing an n-fold pendulum as a composite of n-many pendula.

Categories of lenses/optics and Dialectica categories are both comprised of bidirectional morphisms of basically the same form. In this work we show how they can be considered a special case of an overarching fibrational construction, generalizing Hofstra's construction of Dialectica fibrations and Spivak's construction of generalized lenses. This construction turns a tower of Grothendieck fibrations into another tower of fibrations by iteratively twisting each of the components, using the opposite fibration construction.

We explore a kind of first-order predicate logic with intended semantics in the reals. Compared to other approaches in the literature, we work predominantly in the multiplicative reals \( [0,\infty ] \), showing they support three generations of connectives, that we call non-linear, linear additive, and linear multiplicative. Means and harmonic means emerge as natural candidates for bounded existential and universal quantifiers, and in fact we see they behave as expected in relation to the other logical connectives. We explain this fact through the well-known fact that min/max and arithmetic mean/harmonic mean sit at opposite ends of a spectrum, that of \(p\)-means. We give syntax and semantics for this quantitative predicate logic, and as example applications, we show how softmax is the quantitative semantics of argmax, and Rényi entropy/Hill numbers are additive/multiplicative semantics of the same formula. Indeed, the additive reals also fit into the story by exploiting the Napierian duality \( -\log \dashv 1/\mathrm {exp} \), which highlights a formal distinction between 'additive' and 'multiplicative' quantities. Finally, we describe two attempts at a categorical semantics via enriched hyperdoctrines. We discuss why hyperdoctrines are in fact probably inadequate for this kind of logic.

I will report some work in progress on the semiotics of softmax. This is an operator used in machine learning (but familiar to physicists way before that) to normalize a log-distribution, turning a vector of (thus, a function valued in) logits (i.e. additive reals) into a probability distribution. Its name is due to the fact it acts as a 'probabilistic argmax', since the modes of a softmax distribution reflects the minima (by an accident of duality) of the function. I will show an attempt to make this statement precise, by exhibiting the semantics of a 'very linear logic' on the *-autonomous quantale of extended multiplicative reals. In this logic, additive connectives are also linear, but are still in the same algebraic relation with the multiplicative ones. I will show how to define quantifiers, and thus softmax. If time permits, I'll show a construction of an enriched equipment of relations in which softmax should be characterizable as a Kan lift, in the same way argmax is characterized as a Kan lift in relations.

We illustrate a generalized version of the Para construction which allows to systematically construct triple categories of cybernetic processes, as well as further extensions thereof to cybernetic systems. While Para works for actions in categories, our generalization works for any suitably complete 2-category and for more general notions of action (what we call 'oplax dependent actegories'). To exemplify the construction, we show how applying our generalized Para to the self-action of a monoidal double category of lenses and charts produces a triple category of parametric lenses, lenses and charts which improves on Spivak and Shapiro's Org.

Categories of lenses/optics and Dialectica categories are both comprised of bidirectional morphisms of basically the same form. In this talk I'm going to introduce both and show how they can be considered a special case of an overarching fibrational construction, generalizing Hofstra's construction of Dialectica fibrations. At its highest level of generality, it's a construction that turns a tower of fibrations into another tower of fibrations by twisting each of the components using the opposite fibration construction.

Myers' categorical system theory is a double categorical yoga for describing the compositional structure of open dynamical systems. It unifies and builds on previous work on operadic notions of system theory, and provides a strong conceptual scaffolding for behavioral system theory. However, some of the most interesting systems out have a richer compositional structure than that of dynamical systems. These are cybernetic systems, or in other words, interactive control systems. Notable and motivating examples are strategic games and machine learning models. In this talk I'm going to introduce the tools and language of categorical system theory and outline how categorical cybernetics theory might look like. At the end, we will briefly venture into the triple dimension.

Categorical system theory (in the sense of Myers) is a double categorical yoga for describing the compositional structure of open dynamical systems. It unifies and improves on previous work on operadic notions of system theory, and provides a strong conceptual scaffolding for behavioral system theory. However, some of the most interesting systems out there escape the simple model of dynamical systems. They are instead cybernetic systems, or in other words, controllable dynamical systems. Notable and motivating examples are strategic games and machine learning models. In this talk I'm going to outline an upgrade of categorical system theory to deal with such systems by resorting to triple categories.

We improve the framework of open games with agency by showing how the players' counterfactual analysis giving rise to Nash equilibria can be described in the dynamics of the game itself (hence diegetically), getting rid of devices such as equilibrium predicates. This new approach overlaps almost completely with the way gradient-based learners are specified and trained. Indeed, we show feedback propagation in games can be seen as a form of backpropagation, with a crucial difference explaining the distinctive character of the phenomenology of non-cooperative games. We outline a functorial construction of arena of games, show players form a subsystem over it, and prove that their 'fixpoint behaviours' are Nash equilibria.

Twitter thread about it.

A talk about recent developments on dependent optics. A recording is available on YouTube.

Some developments on dependent optics, prompted by recent advances by Vertechi and Milewski. I obtained the same definition they proposed from a 'dependent' Tambara theory based on actions of double categories, but then shunned it away because I couldn't prove dependent lenses were an example. Vertechi found a way, Milewski found more examples, and thus I released my notes after some updating.

Twitter thread.

A long theory paper on actions of monoidal categories and their properties. We describe distributive laws between monoidal and actegorical structures and provide examples of their use in the theory of optics and parametric morphisms.

Twitter thread.

Using parametric dependent lenses for writing web servers.

Twitter thread.

An outline of some ideas we had lately on the problem of dependent optics, including some solutions.

Twitter thread.

MSP101 introductory talk about optics, focusing in profunctor optics. I also made the notes of the talk into a blog post.

Talk about the Para and Proxy constructions. A companion paper is in the workings.A recording is available here.

Distinguished talk about the eponymous paper.

An invitation to some new and old mathematical gadgets and their use to model cybernetic systems, including but not limited to open games and machine learning.

We show open games cover extensive form games with both perfect and imperfect information. Doing so forces us to address two current weaknesses in open games: the lack of a notion of player and their agency within open games, and the lack of choice operators. Using the former we construct the latter, and these choice operators subsume previous proposed operators for open games, thereby making progress towards a core, canonical and ergonomic calculus of game operators. Collectively these innovations increase the level of compositionality of open games, and demonstrate their expressiveness.

An MSP101 talk about recent developments in the theory of open games, with some speculations about the role of the new machinery for categorical cybernetics.

A TallCat seminar about my master thesis and follow up work. I shows how some notions of stochastic calculus can be internalized in a sheaf topos. Full abstract and recording at the above link.

An MSP101 talk about sheaf theory, covering cohomology and logical applications. There's also an hint of a system-theoretic interpretation I'm working on.

My master thesis work. I explored how stochastic calculus could be simplified by a suitable internalization in a topos of 'stochastic sets'. The results are encouraging, though much remains to be done.