Blog / Technical reports

The concept of initial functor provides a categorical and operational semantics for equational reasoning with diagrams. So far, we have explored this thesis in the simplest possible setting, that of a bare category, or, in logical terms, of an equational theory with unary function symbols. This is rather restrictive. The standard setting for equational reasoning was historically the starting point of both categorical logic (Lawvere 1963) and e-graphs (Nelson 1980; Nelson and Oppen 1980): a category with finite products, viewed as an algebraic theory.

2026-10-14

Discrete vs. filtered accessibility and presentability

Accessible and presentable categories are nice because they make calculating hom sets easy. But not all hom-sets-easily-calculable categories are accessible. In this post we suggest analogous notions, replacing “filtered colimits” with “discrete colimits” (i.e. coproducts), and similarly “compact objects” with “connected objects”. I’ll explain how this sort of accessibility is equally good for calculating.

2026-09-24

Geometric Type Theory, Done Two Ways

A topos can be specified by the geometric theory that it classifies. Though the sequents of a theory are described formally and syntactically, its interaction with the world of sets (through set-indexed disjunctions and axiom schemas) is often a little hand-wavy. In this post I describe two ways of doing this more precisely using type theory.

Mitchell Riley

2026-06-15

CatColab v0.6: Starling

Another few months, another CatColab release! In this post I’ll speak about some new features and fixes found in v0.6: Starling.

2026-06-01

Extending mass-action semantics, Part 2

In the prequel to this post, we saw some benefits of taking a categorical approach to modelling, but also how the process can be fiddly and error-prone, even for a small model. In this short post we describe the implementation of the extended mass-action semantics in CatColab and revisit the model from last time.

2026-04-18

CatColab v0.5: Sandpiper

After 97 days and 96 merged pull requests, CatColab has gone from v0.4: Robin to v0.5: Sandpiper. In this post I’ll walk through some of the main additions, changes, and fixes.

2026-03-23

Extending mass-action semantics, Part 1

One particular use of formal categorical models is for exposition and learning. Indeed, the act of creating one can be a useful exercise for exposing implicit assumptions. In this post, we walk through the process of creating a diagrammatic representation of a system of ODEs and highlight the lessons learnt, as well as pointing towards why tools for formal modelling would be helpful.

2026-03-16

Composition of attractor lattices

This summer at the Topos Institute, under the supervision of Dr. Sophie Libkind, I studied the composition of attractors. The project itself started earlier with my advisor, Dr. William Kalies, who asked me the following question: how do attractor lattices behave when we combine dynamical systems? In this post, I explain how attractor lattices in decoupled product systems can be characterized algebraically in terms of the lattices of their component systems.

Tony Wehbe

2026-01-30

CatColab v0.4: Robin

Since our last blog post about CatColab, we’ve had two releases, meaning we’re now at v0.4: Robin. This brings a few major new features, including compositional notebooks and novel analyses for Petri nets.

2026-01-08

Set-sets

An introduction to endofunctors on Set. Algebras and coalgebras of endofunctors model basic objects of study in mathematics, computer science, and logic. This post explains how to interpret algebras and coalgebras of endofunctors on Set as sets equipped with operations or “co-operations”. We also briefly explore the connection between coalgebra and topology. This is intended as a primer for an upcoming paper about comonads on Set with Kevin Carlson and David Spivak.

Aaron Fairbanks

2025-11-21

DOTS from double theories

Working as a mathematician at Topos means that I spend a lot of time hearing about double categories these days, which are not something that I have much previous familiarity with. In fact, they come up in two seemingly different ways in Topos’ work at the moment: double theories, and double operadic theories of systems (DOTS). In this short post I’ll work through understanding the meaning and purpose of each of these, and then explain one way in which they relate.

2025-11-07

Free PLTL algebras and a coalgebraic extension of hyperdoctrines

categorical logic

This blog post provides an overview of the work I had done with José Siqueira this summer. Inspired by the free Boolean/Heyting algebra of a given set, we develop a free-forgetful adjunction between posets and PLTL temporal algebras, where PLTL denotes propositional linear temporal logic. We provide a description of their induced Eilenberg-Moore categories. We describe how this could be used to temporalise systems and logics through hyperdoctrines and connect this to the stream comonad. We end with future research directions, connecting this topic with the cofree comonad of polynomial functors and temporalising doxastic logic.

Q Le

2025-09-26

Incremental query updating in adhesive categories

acsets

databases

Working in the general setting of adhesive categories, we derive a practical algorithm for incrementally updating a query’s results with respect to small changes in the object being queried.

2025-08-15

Substitution is also pushout

How we can think about pushouts as applying rules via substitution, featuring examples in categorical databases and Datalog.

2025-08-06

CatColab for Model Building

crosspost

Nate Osgood, together with 4 students from the Computational Epidemiology and Public Health Informatics Lab in Saskatoon, Canada, recently ran a community group model building event focusing on the drivers for homelessness in their city. This post describes the event, and the next steps that they are planning to take.

Nathaniel Osgood

2025-07-18

Liberating synthetic quasi-coherence from forcing

topos theory

In this blog post, I’ll reformulate Ingo Blechschmidt’s “synthetic quasi-coherence” axiom — or more precisely his “general nullstellensatz” — as a lifting property inspired by Ivan Di Liberti’s work on coherent toposes and ultrastructures. This lifting property shows that synthetic quasi-coherence can be derived from a sort of “directed path induction” for toposes, suggesting the possibility of an internal logic for all toposes in which the axioms for any sort of synthetic mathematics would compute. (Based on joint work with Mitchell Riley)

2025-07-13

In this blog post we consider the practical tradition of Euclid’s elements, in contrast to its more familiar role as a model of axioms and proof. Inspired by that tradition and combining it with the notion of wiring diagrams we propose an abstract model to think about and problem solve issues of manufacturing, especially using the power of modern digital manufacturing tools.

Edmund Harriss

2025-04-30

Distilling Research at Scale

technology

vision

New concepts must be explained to be understood, yet we rarely invest sufficient effort in clarifying them. While explanations demand time and care, this investment is essential, because without it, ideas remain opaque, inaccessible, and dormant. Today we see that the pace of explanation production has not kept up with the volume of knowledge production, resulting in a growing “research debt”: “the accumulation of missing interpretive labor”. To address this, we need deliberate, focused measures to resolve our intellectual deficits. This essay proposes the concept of “cognitive compilers,” an overarching effort to translate technical research complexity into its most accessible forms — for the sake of discovery — in a scalable way.

Hamidah Oderinwale

2025-04-04

CatColab 0.2: Wren

Today we’re excited to announce the first alpha release of CatColab 0.2: Wren. CatColab is software for making models of the world together.

Kevin Carlson

2025-02-05

Polynomial universes and natural models

In this post, I summarize the work I conducted over the summer of 2024 at the Topos Institute, together with David Spivak, wherein we have aimed to extend, refine, and generalize the treatment of models of type theory in terms of polynomial functors via the concept of polynomial universes. We shall see how the language of polynomial functors can be used to elegantly capture all of the usual constructs of dependent type theory, and moreover, how interpreting this language in homotopy type theory reveals striking properties of these structures.

C.B. Aberlé

2024-12-10

Structure-aware version control via observational bridge types

In this post, we suggest a way to use observational bridge types (as in the Narya proof assistant) for structure aware version control.

2024-11-13

Neural wiring diagrams for message passing in multiscale organizations

operads

In our recent paper, “Dynamic task delegation for hierarchical agents”, Sophie Libkind and I described a task delegation from an agent to a team of subordinates as morphisms in a certain operad called \mathbb{O}\mathbf{rg}_{\mathfrak{m}}. However, such morphisms include a great deal of data, and the examples we gave there barely scratched the surface of what’s possible. In this post I’ll show how “recumbent” neural wiring diagrams—with arbitrary feedback and “axon” splitting—give rise to a message-passing language for describing certain such task delegations. That is, I’ll define a cyclic operad \mathbf{rnWD} and a functor \mathbf{rnWD}\to\mathbb{O}\mathbf{rg}_{\mathfrak{m}}.

2024-11-08

Declarative Models and Collaborative Modeling

hiring

Although we at the Topos Institute spend much of our days applying category theory, underlying our activities is a philosophy around the activity of science and engineering that is not explicitly category-theoretic in nature. In this blog post, we lay out some of the core ideas of this philosophy, and tie them in to current and future research developments at Topos.

2024-10-31

Taking nonlogical concepts seriously

vision

language

philosophy

What is the right math to capture our concepts which don’t have formal definitions? Recent work in philosophy of language clarifies the relationship between logic and good reasoning, with consequences for science, applied math, and AI. In this post we will introduce logical expressivism, its underlying mathematics, and a vision for how it can support software with novel affordances for communication and integration.

2024-10-11

Open curricula and assessment tools workshop in Kisumu

community

technology

In August, Brendan and I attended the American Institute of Mathematics workshop “Open source mathematics curriculum and assessment tools”, hosted by Maseno University in Kisumu, Kenya. The workshop was a fantastic opportunity to meet new specialists in a variety of domains and hear about what they were working on. This post is a short summary on the workshop and what we learnt.

2024-09-06

Wiring diagrams for Mealy machines

Operad algebras are a known tool for the composition of dynamical systems, but what happens when we have a machine where the output of the machine also depends on the input into it? In this post, we give background on how we want to extend the operad of directed wiring diagrams to the operad of dependent directed wiring diagrams, and then use this to be able to compose these kinds of machines.

Keri D’Angelo

2024-08-19

A polynomial account of Bayesian update

Sophie Libkind, David Spivak

One of the things I do at Topos is make sense of some aspect of the world by articulating it in mathematics. Follow along as I make sense of Bayesian update using the mathematics of polynomial functors.

2024-08-12

How to write a fantastic book in four months, Part III

outreach

Priyaa Varshinee Srinivasan

In the third post of this series about Relational Thinking: from abstractions to applications, we look at the story-telling approach that we took in writing the book.

2024-07-09

How to write a fantastic book in four months, Part II

outreach

Priyaa Varshinee Srinivasan

In the second post of this series about Relational Thinking: from abstractions to applications, we look at the technologies used to build the book.

2024-07-04

How to write a fantastic book in four months, Part I

outreach

Priyaa Varshinee Srinivasan

In the first post of this series, we introduce the freely available online book Relational Thinking: from abstractions to applications, starting with the story of how it came into being and giving a brief overview of its contents.

2024-06-28

Toward compact double categories: Part 2

Last time we framed the puzzle of axiomatizing categorical duality and introduced new double-categorical tools, culminating with the twisted Hom functor. We’ll now get straight to the point by proposing a definition of a compact double category. After that we’ll fill in a few remaining technical details. More interestingly, we will examine the key examples and find that in all cases a compact double category, unlike a compact bicategory, uniquely determines the dual objects up to equivalence, even isomorphism.

2024-06-24

Toward compact double categories: Part 1

Lately I’ve been pursuing formal category theory using double categories. A first step in this program is to abstract from categories to category objects in a double category; for instance, internal categories are category objects in a double category of spans and enriched categories are category objects in a double category of matrices. The next step is to take structures defined on categories and generalize them to category objects in a double category. By the microcosm principle, that is possible when the double category possesses a categorified version of the very structure in question. The concepts from double category theory that I’ve used so far, like products and coproducts, indeed categorify familiar concepts from category theory. While there are interesting twists along the way,¹ the one-dimensional story gives strong hints about how to generalize to double categories.

2024-06-20

Ontological Commitments for Boundaries

When we do math about things we care about, committing to which mathematics represents which intuitions moves us forward.

Sophie Libkind

2024-04-25

Understanding UMAP

data science

UMAP is a dimension-reduction method that has become very popular, especially in many areas of biology. Recently, a certain figure produced by UMAP has been circulated online to support spurious conclusions about “genetic racial groups”, or, to put it more bluntly, to support scientific racism. In the original paper outlining the method, the section justifying the construction uses a lot of category theory, which many practicing scientists might not be comfortable with. The purpose of this post is simple: much online discussion is stymied by the fact that UMAP is a opaque process for people not comfortable with the language of category theory; can we unpack things in less technical language? As a result, we can more critically evaluate any claims concerning UMAP and “interpretability”.

2024-04-05

Algebras are promonads

An interesting analogy between algebras over a ring and promonads on a category is formalized using the apparatus of double theories.

2024-01-29

Composing springs

Physical systems are often composed of many interacting subsystems. In this post, we take a peek at the math and the software implementation for composing systems of springs using decorated cospans.

Sophie Libkind

2024-01-18

Why double categories? Part 1

databases

The beginning of a series of posts answering the question “why double categories?”. Our first answer is that double categories give the algebra of relations from universal properties.

2024-01-15

Building dynamic structures

In our day-to-day lives, we all interact with many systems where the structure of the system changes based on external or internal factors. How do we make sense of structures that can change in this way? In mathematics, we often assume the structure we’re working with is “fixed” to some extent, and here we want the exact opposite: structures that can change. This summer, as part of Topos’ 2023 Summer Science Research Associates cohort, I spent a lot of time with David thinking about and working on this problem, and I’m excited to discuss a streamlined mathematical approach to describing and building structures that can be updated in this way.

Samantha Jarvis

2024-01-09

Poly-morphic effect handlers

Harrison Grodin, David Spivak

In computer science, programmers often perform effects to interact with the surrounding environment. For example, a program may print strings or interact with mutable state. Then, effects may be handled, implemented in terms of other effects. In this post, we reconstruct a categorical semantics for programs with effects, and we isolate a class of composable effect handlers that may be concisely described in the language of polynomial functors, the free monad monad, and the Grothendieck construction.

2024-01-03

Responsible mathematics and metaphors of semantics

philosophy

language

An exposition of a philosophical argument about how words connect with their meanings, and a tentative connection to work done at Topos.

2023-12-14

Categorical Statistics in Julia

statistics

This summer I created the StatisticalTheories.jl package so we can do categorical probability and synthesize probabilistic programs in the AlgebraicJulia ecosystem. Read all about it!

Harper Hults

2023-11-28

Introducing InterTypes

acsets

crosspost

Announcing the first version of InterTypes: a package for cross-language serialization for ADTs and ACSets

2023-11-14

Solving problem-solving

Priyaa Varshinee Srinivasan, David Spivak

Our physical world is incredibly complex. Surviving life is a lot about problem-solving, be it waking up in morning and finding your way to the bathroom or solving a math problem for research. We constantly abstract information back and forth from the physical plane to our mental plane for solving these problems. Today I am interested in showing you a way to formalize problem-solving — more specifically, telling the translation story using category theory — and seeing if such abstraction will help enhance the process.

2023-11-13

Lie groups induce Hopf monoids in Poly

geometry

A Lie group G is a group object in the category of manifolds; that is, it’s a smooth space equipped with a special point e:G and a multiplication operation G\times G\to G. Every manifold M has a cotangent bundle T^*M\to M, and this can be made into a polynomial functor t^*_M. In this post we note what may be considered pretty obvious in retrospect: the polynomial t^*_G induced by the cotangent bundle on any Lie group G has the structure of a Hopf monoid.

Succinctly, a Hopf monoid is a bimonoid (i.e. it comes equipped with multiplication and comultiplication maps t^*_G\otimes t^*_G\to t^*_G and t^*_G\to t^*_G\otimes t^*_G, and unit and counit maps \mathcal{y}\to t^*_G and t^*_G\to\mathcal{y}, satisfying the usual equations) together with an antipode t^*_G\to t^*_G. The idea is to internalize the notion of a group in any monoidal category; in our case (\mathbf{Poly},\mathcal{y},\otimes).

I’ll explain the above in this post. In fact, we’ll see that the Hopf monoid leaves out a bit of the structure held by Lie groups, so we’ll append a bit more structure onto our Hopf monoids to capture it. Finally, we’ll explain what all this has to do with dynamic organizations, such as those found in deep learning and prediction markets.

2023-10-26

Retrotransformations

Retrotransformations between lax double functors are introduced as the “multi-object” analogue of a cofunctor between categories. Notions of “monoidal cofunctor” between monoidal categories and of “multicofunctor” between multicategories are then derived as special cases.

2023-10-20

Cartesian double theories

Cartesian double theories are a new framework for doctrines based on double-categorical functorial semantics.

2023-10-13

Powers of polynomial monads

Many of our favorite monads on \mathbf{Set}, such as the Maybe monad and the List monad, are polynomial. It turns out that monads have special “powers” in \mathbf{Poly}.

The category \mathbf{Poly} is cartesian closed, and in particular, we can raise one polynomial q to the “power” of another polynomial p—or exponentiate q by p—to obtain q^p. It turns out that this operation is very interesting when q=t is a monad: exponentiating a monad is lax monoidal with respect to two different monoidal structures on \mathbf{Poly}, namely \times and \mathbin{\triangleleft}. In particular, we have natural maps t^p\times t^q\to t^{p\mathbin{\triangleleft} q} and t^p\mathbin{\triangleleft} t^q\to t^{p\times q}.

In this post I’ll explain how exponentiation in \mathbf{Poly} works and how it feels, as well as what special thing happens when the base is a monad t. Then I’ll give an application: raising a polynomial monad to the power of a polynomial comonad (small category) results in something that’s both a monad and a \times-monoid.

2023-09-21

Unbiased monoidal categories are pseudo-elements

operads

Categorifying the observation that monoids are generalized elements of multicategories, we show that unbiased pseudomonoids, such as unbiased monoidal categories, are “pseudo-elements” of 2-multicategories.

2023-08-15

A nuclear adjunction between Poly and Dir

There are at least two interesting kinds of maps between bundles: “forward-forward” maps and “forward-backward” maps. That is, both kinds go forward on the base, but the first kind also goes forward on the fibers, whereas the second kind goes backwards on the fibers. In a paper with David Jaz Myers, we showed (for bundles of sets) that the first category is equivalent to \mathbf{Dir}, the category of Dirichlet polynomials, which are sums \sum_{b:B}(E_b)^\mathcal{y} of representables \mathbf{Set}^\textnormal{op}\to\mathbf{Set}; the second category is equivalent to \mathbf{Poly}, the category of ordinary (Descartes) polymomials, which are sums \sum_{b:B}\mathcal{y}^{E_b} of representables \mathbf{Set}\to\mathbf{Set}.

Recently I realized that for any set X, there’s an adjunction L_X\colon\mathbf{Dir}\rightleftarrows\mathbf{Poly}\colon R_X. Moreover, when |X|\geq 2 has at least two elements, this adjunction is nuclear, i.e. it’s both monadic and comonadic. In particular, this means that you can model \mathbf{Dir} inside of \mathbf{Poly} as the coalgebras for a certain comonad on \mathbf{Poly}, and you can similarly model \mathbf{Poly} inside of \mathbf{Dir} as the algebras for a monad on \mathbf{Dir}. I’m not sure if this has any practical applications, but it’s at least theoretically interesting. And when X=0, I’ll show how the coalgebras model “sets with elements marked for deletion”.

2023-07-21

Agent-based modeling via graph rewriting

Rewrite rules are organized via a graphical syntax into discrete-time simulations which can be understood as agent-based models. This representation is transparent, compositional, and serializable.

2023-07-07

Acsets with variables

Acsets are great, but what if attributes could be variables?

Kris Brown, Kevin Arlin

2023-06-20

Natural transformations between cofunctors

Polynomial comonads can be identified with categories, but the morphisms between them are not functors; they’re called cofunctors. There is a reasonable notion of natural transformation between cofunctors, but I always found remembering how it goes to be a slog. Recently I realized that they have a very reasonable form in terms of polynomial comonads. In this short post, I’ll introduce the subject, give the formula for natural transformations between cofunctors and explain it, discuss identities and compositions, and then conclude with a summary.

2023-05-26

Categories for Epidemiology

Xiaoyan Li, Sophie Libkind, Nathaniel D. Osgood, Eric Redekopp and I have been creating software for modeling the spread of disease… with the help of category theory! Lots of epidemiologists use “stock-flow diagrams” to describe ordinary differential equation (ODE) models of disease dynamics. We’ve created two tools to help them. But what’s a stock-flow diagram, and what does our software let you do with them?

John Baez

2023-05-12

Symbolic presentations of dynamical systems

geometry

crosspost

A follow-up to “Algebraic Geometry for the Working Programmer”, this post explains a category-theoretic approach to symbolic open dynamical systems.

2023-05-08

Spooling out syntax from behavior

The behavior of a dynamical system is its entire fate or character: the tree consisting of precisely what it will do when exposed to any particular sequence of inputs. In the world of polynomial functors, behavior for a dynamical system with interface p is formalized using the cofree comonad \mathfrak{c}_p. On the other hand, syntax in a given language p is formalized using the free monad \mathfrak{m}_p. In this post we explain a sense in which one can extract syntax from behavior: briefly, given a map q\mathbin{\triangleleft}p\to p\mathbin{\triangleleft}q, you get a map \mathfrak{c}_{p\mathbin{\triangleleft} q}\to\mathfrak{c}_p\mathbin{\triangleleft}\mathfrak{m}_q, which we call the associated spooling map. We give a variety of examples, a bit of basic theory, and a program—written entirely as a few arrows of \mathbf{Poly}—for computing conditioned probabilities and expected value of a repeating lottery system.

2023-04-24

Conegation rewriting

Rewriting theory studies rules for turning things into other things. Typically, one considers various types of graph, and looks at rewriting rules that have a form like this: “whenever you see a subgraph shaped like I, replace it with one shaped like O, using the common subgraph K to attach it”. It turns out that this informally-sketched procedure is somewhat ambiguous, and rewriting theorists have developed a few different ways of resolving the edges cases. In this post, I’ll briefly sketch this picture, and introduce a new type of graph rewriting: “conegation rewriting”.

Eigel Rischel

2023-04-11

Imperative Programming with Poly

Category theory has been applied fruitfully to functional programming for decades, leading some to think that functional programming represents the one true way of doing math on a computer. However, the stubborn fact that the internals of computers and the world itself are both stateful means that imperative programming is darn useful. And following my ACT motto of “if the practitioners are doing it, they can do it better with category theory”… comes the flow of research that lead to this blog post.

2023-04-05

Seventy Years Using Fixed Points

lambda calculus

Having first heard about theorems on fixed points as an undergraduate, uses for them came into my research on many subsequent occasions. The talk will review some personal history and give some suggestions for possible further applications.

Dana Scott

2023-03-29

Algebraic geometry for the working programmer

In this series of posts, we investigate the duality between algebra and geometry in order to develop new types of lenses. In this first post, we review some basic ideas about algebraic geometry that will be needed in the coming posts.

2023-03-23

Lotteries: a constructive version of the distributions monad

Many category theorists have heard of the distributions monad \mathsf{dist}\colon\mathbf{Set}\to\mathbf{Set}, which sends a set X to the set of finitely supported probability distributions on X. Many have also heard of the operad \Delta of simplices, for which an n-ary operation is a probability distribution on n elements. This operad \Delta corresponds to a certain polynomial monad on \mathbf{Set}, which I’ll denote \mathsf{lott}. What monad is it, and how does it compare to \mathsf{dist}? In this post I’ll explain how to think of it as a monad of lotteries, where the number of tickets—like sides of a coin or faces of a die—are known in advance. I’ll also explain its relation to \mathsf{dist} and how conditioning looks in this setting.

2023-03-23

Structured cospans as a cocartesian equipment

The theory of structured cospans is dramatically simplified by the use of double-categorical universal properties. Specifically, we show that structured cospans form a cocartesian equipment, a result that is stronger yet easier to prove than the usual result that they form a symmetric monoidal double category.

2023-03-15

Promonoidal categories and wiring diagrams

operads

There are (colored) operads for all sorts of different flavors of wiring diagrams: those governing monoidal categories, symmetric monoidal categories, traced categories, compact closed categories, hypergraph categories, etc. But all of these operads are in fact more than mere operads: there’s a sense in which you can take any operation, cluster together various objects in it, and thereby factor the operation. Operads are about how operations compose, but we seem to be able to factor, or decompose operations. What gives? At a recent workshop, Mario Román explained pro-monoidal categories to me, and he conjectured that wiring diagram operads are pro-monoidal; I agree and, though I haven’t proven it, I’ll present the conjectural idea below.

2023-01-31

Recursive Types via Domain Theory

lambda calculus

Functional programming languages often include recursive types, allowing programmers to define types satisfying a given isomorphism. Such types cannot all be interpreted as sets, but they can be understood using domain theory. We consolidate and present foundational techniques in domain theory to understand eager programming languages with recursive types from a categorical perspective. We define a category of domains with finite coproducts, a symmetric monoidal closed structure for eager products and functions, and least solutions of recursive domain equations, whose objects are retracts of a universal space and whose morphisms are continuous with respect to a topology of approximations.

Harrison Grodin

2023-01-10

Preparing for Networked Mathematics

MathFoldr

LLMs

NLP

Networked mathematics is one of my main projects at the Topos Institute (the other is Dialectica categories and its extended family of formalisms). We have not had much luck getting the funding agencies to pay attention to it, yet. But the work is progressing, albeit slowly. We have been working on the suggestion that formalized mathematics will eventually be one of the main ways of producing mathematics. It seems sensible to believe that proof assistants will become really useful tools for mathematicians, and if so, formalized math will become the usual practice, not the exception. To discuss the issues of formalized mathematics and to prepare for the Hausdorff Institute of Mathematics trimester on “Prospects of Formal Mathematics” in 2024 we have had in the Topos Colloquium talks by several people involved with proof assistants and automated deduction.

Valeria de Paiva

2023-01-05

Lenses are semi-monads, maybe lenses are monads

lenses

Have you ever heard of a semi-monad? I hadn’t, but when I came across a “monad without unit” in the wild, I made an analogy with semigroups (a semigroup is a group without unit). It seems others have also thought to use the term semi-monad for such a gadget. There is a semi-monad structure on the full subcategory of lenses inside Poly, and this is useful for building logic circuits and other interconnected dynamical systems. In particular, it allows us to formalize what I think is really pretty notation for “speeding up” boxes in wiring diagrams. But what does this mean mathematically? We’ll explain in this post.

2022-12-20

Dialectica Categories in Computing

dialectica

events

In the first half of the year we had an AMS Mathematical Research Community (MRC) on Applied Category Theory, in Beaver Hollow, NY. An MRC is a bit like a version “on steroids” of the ACT Adjoint School, as there are many more researchers in a research subgroup in the MRC than in a Adjoint School group. While my ACT Adjoint School group had four students and a TA, my MRC group had thirteen researchers. So from four to thirteen people you have more than three times the number of people to do interesting research with. This post was meant to be about the four subgroups we split into and why I am so excited for the mathematics we’re doing. But I am a bit behind with my processing of the knowledge we shared when people visited here (and over Zulip!). So, while I could possibly wait for the JMM to get to grips with more of the new math that people are producing, I think I will try to explain, at least a little, how the themes above interact.

Valeria de Paiva

2022-12-06

Scott’s model of lambda calculus

lambda calculus

Valeria de Paiva, Jacob Collard

Lambda calculus constructs a set of terms starting from a set of variables using operations and rules. If we treat lambda calculus as a programming language, we can consider a model as a way of giving an implementation of lambda calculus. This essentially gives an implementation of a typed programming language with product types, function types and certain inductive types.

Anthony Agwu

2022-11-23

Mathematical concepts: how do you recognize them?

Humans are very good at recognizing the words they do not know, the concepts they haven’t met yet. To help with these they invented dictionaries, glossaries, encyclopedias, wikipedias, crib sheets, etc. Initially, they did it via laborious manual work, more recently through automated construction techniques. Natural language processing (NLP) tools have improved impressively in the last decade. Most of this incredible improvement happened to newspaper text and hence named entities of the kind found in news text can be detected and classified (usually into people, organizations, places and dates) with much greater accuracy than in the recent past. However, for domain specific text, like the academic literature in different sciences (e.g. Medicine, Biology, Chemistry), or in the Humanities(History, Sociology, Philosophy, etc.) things are more complicated. Thus extracting technical terms/concepts from papers is important, interesting and usually difficult. How do you detect mathematical concepts in text?

2022-11-16

When you light up, I light up

Sophie Libkind, David Spivak

“Cells that fire together, wire together.” This slogan for Hebbian learning evokes a strategy for reorganization in which an individual strengthens their connection with another if they have similar behavior. Here we give a mathematical account of Hebbian learning as a dynamic monoidal category.

2022-10-28

Project cards: a tool for research transparency

ethics

This blogpost presents some early-stage, exploratory work on a kind of tool that may be useful for Topos (and other similar institutes!) as it matures as a company. In a nutshell, it is meant to serve as a framework to facilitate accessibility and discussion—internally and externally—of the various projects under development here.

Alejandra Arciniegas

2022-10-24

Nate & Jesse’s adjoint 5-tuple

In August, Nate Soares visited the Topos Institute. We told him a little about Poly and Proly, and he told us about what he wanted from a type theory. Probably the high point in the discussion for me is when he drew the following picture of what he wanted from a type theory.

2022-09-29

Using categorical logic for AI planning

LLMs

acsets

It’s breakfast time! You wake up and walk to your kitchen and notice a loaf of bread, a knife, a raw egg (in its shell), a skillet, and a stove burner sitting on the counter. You’re hungry and your preferred state of existence is to, instead, have an egg sandwich sitting on your counter. You are saddened by the situation, but feel empowered to change it! You compare what you have and what you want, recall what cooking skills you have, and devise the following steps:

Angeline Aguinaldo

2022-09-20

A dynamic monoidal category for strategic games

lenses

After last month’s wonderful ACT conference at University of Strathclyde in Glasgow, David Spivak and I spent some time with Matteo Capucci and Riu Rodriguez Sakamoto talking about how our theory of dynamic monoidal categories can model the non-cooperative strategic games that they study at Strathclyde. A dynamic monoidal category is an elegant way to formalize a version of compositional game theory based on Matteo’s work in, where games can be composed both sequentially and in parallel with the players updating their strategies by applying “counterfactual reasoning” to their payoffs in a functorial way.

Brandon Shapiro

2022-09-12

Data Operations are Functorial Semantics

Alejandra Arciniegas, Brendan Fong

databases

Double categories illustrate that data munging is functorial semantics. This post reviews the functional and relational approaches to ologs and database schemas. Double-categorical ologs are meant to incorporate aspects of each. These should also be viewed as double-categorical database schemas and a data instance is a structure-preserving double functor valued in relations. Double-categorical ologs will be cartesian equipments which may or may not be asked to have tabulators. Viewing a double category as a theory and an instance as a model, usual data operations such as select, filter and join are seen to be captured as a result of the fact that the data instance is structure-preserving. This is illustrated via a number of examples.

Michael Lambert

2022-09-06

Strategies for ethically oriented pursuit of research and technology

ethics

At Topos we’re motivated to build technologies that help us understand the complexity of the systems around us, and to cooperate to improve them, for everyone’s sake. But sometimes good intentions are not quite enough. For example, cooperation requires trust, and we want our technologies to help build trust within society. It’s now clear that technologies like social media can damage trust through misinformation and polarization. How might we anticipate and protect against such consequences in our own work?

2022-08-24

Imagining Bicomodules with Type Theory

Some say that the objects of mathematics really exist in some Platonic realm, and some say they are fictions in the minds of mathematicians. Either way, it is evident that they cannot be directly grasped with the ordinary five senses. Nobody has ever seen a perfect circle or a natural number. Rather, we grasp the objects of mathematics by means of imagination. I set out to imagine bicomodules in Poly (aka prafunctors) in this way, as they are an important and powerful feature of the Poly ecosystem. This blog post shows what I have come up with. As it turned out, the result is not only suitable for imagination, but also for implementation in computers (digital imagination, perhaps?) Indeed, we’ll see bicomodules as an essentially algebraic theory and discuss how it is used for data migration.

Joshua Meyers

2022-08-19

It’s Proly like Poly but better

Every mathematician I talk to agrees that Poly is an incredibly rich category. How could they not: it’s complete, cocomplete, three orthogonal factorization systems, two monoidal closed structures, its comonoids are categories, etc. And yet there is a common complaint about it, when it comes to modeling. Namely: it’s somehow very discrete, very anchored to Set. Luckily, it looks like the days of disappointing discreteness are behind us. I now think I’ve spent the last 2.5 years enamored by a pale reflection of “the real Poly”, namely what Brandon and I have been calling Proly. I’ll tell you all about it below.

2022-08-04

Dialectica categories and polynomial functors, Part 1

dialectica

Like many stories in math, this one is about building bridges: uniting the dialectica categories from Valeria’s 1991 doctoral thesis with David’s work on polynomial functors. I’ve been working with David on polynomial functors for two years now, so when I was placed in Valeria’s team at the AMS’s 2022 Mathematics Research Communities Conference Week on Applied Category Theory, it was only natural that I try to tie their two perspectives together. There, under the guidance of Valeria and her trusty deputy Jérémie Koenig, I had the pleasure of leading a mini-research team consisting of Samantha Jarvis and Joseph Dorta in connecting dialectica categories to polynomial functors. Our launchpad was Sean Moss’s talk from the 2022 Workshop on Polynomial Functors. In this first post of a series, I’ll start by reviewing his work, before giving you a peek at what we found; we’ll have even more to share next time.

Nelson Niu

2022-07-12

A 15-year history of my research program, in 10 minutes

This post presents a video presentation, originally shown to the Topos Board of Directors, about David’s research program over the past 15 years, from 2007 to present.

2022-07-07

Graphs in Poly

It’s really amazing to me that comonoids in Poly are categories, and I think it would be cool if more people understood that on a gut level. But explaining it takes more time than people are sometimes prepared to give. So today, I want to explain a much simpler case—one which gives a lot of the intuition—namely that of graphs.

2022-06-16

Decorated cospans via the Grothendieck construction

Building on the double Grothendieck construction introduced last time, we explain how decorated cospans are instance of the Grothendieck construction. This perspective suggests a natural generalization of decorated cospans, which we illustrate through several examples.

2022-05-30

Grothendieck construction for double categories

What is the Grothendieck construction for double categories? We explore one possible answer to this question, based on the perspective that double categories are categories internal to \mathsf{Cat}. In fact, we suggest a general procedure for doing the Grothendieck construction on any structure that is defined internally to \mathsf{Cat}.

2022-05-23

The many facets of Networked Mathematics

MathFoldr

LLMs

NLP

Last year we started a discussion on the production of mathematics, the pre-industrial kind of process that we all still follow of solving problems and taking the solutions to the market of ideas (conferences, seminars, blog posts, twitter, coffee breaks in the department, etc.) as drafts/preprints/submissions and all the difficulties that this process involves. In particular we discussed the difficulties of checking whether the work had been done before or not, and the difficulties of searching for other, similar work that might help us with a given question. In this blog post we give an update on our project.

Valeria de Paiva

2022-04-18

Diagrammatic equations and multiphysics, Part 2

physics

Tim Hosgood, Evan Patterson

Previously, we surveyed some of the fundamental concepts from our paper on the use of diagrams to present equations from mathematical physics. In this blog post we take a look at how we can enrich our framework, introducing cartesian and symmetric monoidal products in order to be able to express more complicated (e.g. non-linear) systems of equations. We also take a look at how we can use undirected wiring diagrams to build up multiphysics models from smaller constituent pieces. Finally, we have a look at some of the interesting questions in pure category that arise from this subject.

2022-04-15

Diagrammatic equations and multiphysics, Part 1

physics

Tim Hosgood, Evan Patterson

Using diagrams to encode equations between physical quantities is something that has become more and more common over the past few decades. To a category theorist, however, the use of such diagrams is not as formal as one would perhaps like. In this new paper, we fix this problem: systematising the use of diagrams in expressing multiphysics models and their solutions via a categorical framework.

2022-04-08

Co-design of dynamical systems

In 2015, Andrea Censi invented a beautiful category-theoretic way to collaboratively and computationally design new things under complex systems of constraints. For example, suppose that a robot is made of a chassis and a motor. Since the motor powers the chassis and the chassis carries the motor, you could ask: is it worthwhile to use a more powerful motor, even if it weighs more?

2022-04-06

Creating new categories from old: Selection categories

In this short post, I’ll describe a way of creating new categories from old. It reminds me of a ‘particle filter’ or ‘natural selection’. This method comes from the theory of polynomial functors, but I’ll confine all the technical details to a single section, so you don’t need to know anything about polynomial functors to read this post.

2021-12-30

Left adjoints, lenses, and localisation

lenses

geometry

In this post I am going to recount three stories that I’ve been thinking about recently: Cauchy completion, internal lenses, and GZ/zigzag-localisation. The first two of these stories are probably more likely to be familiar to the (applied) category theory audience of this blog than the third. For me, coming from the “opposite” background, the first two seem to have the same flavour as the third, and that is the purpose of me writing this: I’m hoping that somebody out there will be able to tell me what the underlying formalism is. I’ll end this post with a specific “conjecture” (really, just a question), that I would imagine is some sort of folklore result (in that, I can’t find it written down anywhere, but it seems very much alluded to in lots of places).

2021-11-24

Deep neural networks as nested dynamical systems

Tim Hosgood, David Spivak

This week, we (David Spivak and Tim Hosgood) uploaded a new paper to the arXiv: “Deep neural networks as nested dynamical systems”. In it, we discuss how to think of both deep neural networks and interacting dynamical systems as some encompassing generalisation, which we call deeply interactive learning systems. The paper is rather short, and hopefully more accessible than technical, so we won’t paraphrase the main story here, but will include the introduction below to save you clicking through!

2021-11-05

Categorical systems theory

Categorical systems theory is the study of the design and analysis of systems using category theory. Category theory is a hopelessly abstract branch of pure mathematics, so abstract that even the other mathematicians refer to it as “abstract nonsense”. Why would anyone want to study such complex and concrete situations as general systems with a branch of mathematics so divorced from reality? In this blog post, I hope to answer that question. I want to say what the point of doing systems theory categorically is; what the main take-away lesson is, beyond the technicalities. I also want to show that category theory isn’t divorced from reality at all; it’s just general purpose.

2021-11-04

Poly inside Poly

In this post, I’ll explain how to use Steve Awodey’s notion of universe to represent the set of polynomials as a certain naturally-derived object in Poly: “Poly inside Poly”. That is, given a universe u there’s an associated polynomial functor w that encodes u-small polynomials, and also encodes the closure of u-small polynomials under dependent sums and products, and under various other operations.

2021-09-22

Compositional Thermostatics

physics

In this post, we explore the compositionality of thermodynamic systems at equilibrium (thermostatic systems). The main body of this uses no category theory, and reviews the physics of thermostatic systems in a formalism that puts entropy first. Then there is a brief teaser at the end showing how this entropy-first approach can be treated categorically.

2021-09-09

Enriched categories as dynamical systems

video

Often in applied category theory, we hear about how systems form categories — categories of systems. But what about when the systems are categories? In this lecture, we introduce the idea of enriched categories, taking the point of view that an enriched category is a sort of dynamical system.

2021-09-02

Dirichlet polynomials and entropy

Tim Hosgood, David Spivak

Recently, we (David Spivak and Tim Hosgood) put a preprint on the arXiv called “Dirichlet polynomials and entropy”, which explains how to recover Shannon entropy from a rig homomorphism involving the weighted geometric mean. In this blog post, we explain the main story, from a slightly different point of view as found in the preprint: starting with Dirichlet polynomials, seeing how they corresponds to set-theoretic bundles, and then looking at how Huffman coding can help us to rediscover the notion of entropy.

2021-07-25

Introducing the MathFoldr Project

At Topos we believe knowledge empowers people, and that our community’s expertise should be available to all who seek it out. But simple availability is not enough. True access is more than an open door: it’s clear, legible street signs, elevators, and gently sloping on-ramps. And with modern AI and natural language processing tools, we believe it’s beyond time to build these accessibility tools for science and mathematics. This blog post provides an overview of our nascent MathFoldr project, sharing our dreams and our approach so far, and even, at the end, a chance for you to get involved!

Brendan Fong, Valeria de Paiva

2021-07-11

Jump monads: from conjugation to dependent types

The world of polynomial functors often seems so rich that it should contain the whole universe, and there are some tantalizing suggestions that, in fact, it does. Given a dependent type theory, we can follow Steve Awodey and encode its syntax into a “universe polynomial” indexed by the types of the theory, and whose summands represent the terms of each type. How far can we follow this idea? How does dependent type theory relate to the categorical structure of polynomials?