 ## By Pavel Panchekha

### 18 August 2018

Share under CC-BY-SA.

# Not Quite Pushouts

In my last post, I proved a neat little theorem in category theory: that if $$C$$ and $$D$$ are categories with pushouts, then the category $$C \to D$$ of pushout-preserving functors from $$C$$ to $$D$$ itself has pushouts. Here, I'm going to develop a construct similar to pushouts, but a little more general.

## Generalized pushouts

A pushout is a construction you might be able to perform in a category on two arrows $$f$$ and $$g$$ that have a common source. If $$f : A \to B$$ and $$g : A \to C$$, then the pushout provides an object $$D$$, written $$B +_A C$$, and arrows $$f' : C \to D$$ and $$g' : B \to D$$, such that $$f g' = g f'$$,1 [1 Where adjacency is reverse composition.] and such that $$D$$ is universal with regard to this property.

For my goal, which I described in my last blog post as functional reactive programming with operational transform, the pushout is unfortunately too restrictive. The universality property means that there is usually a unique choice of pushout, and it's not always the one that I as a programmer would like. I want a construction that still produces an $$f'$$ and a $$g'$$, but gives me more choices about what those are.

My replacement construction is what I call a concurrent category. A concurrent category is a category $$C$$ plus a functor $$T : C → \mathbf{CAT}$$, which maps $$a : C$$ to the under category $$a / C$$. In other words, this is a category $$C$$, plus the ability to take an arrow $$f : a \to b : C$$, and map it to the functor $$T(f) : a / C \to b / C$$, or, unpacking this definition further, it is a category $$C$$ plus the ability to take arrows $$f : a \to b$$ and $$g : a \to c$$, and produce functions $$f' = T(g, f) : c \to d$$ and $$g' = T(f, g) : b \to d$$. As an additional condition, the functor $$T$$ is may have the property that $$g T(g, f) = f T(f, g)$$; in other words, $$f$$, $$g$$, $$f'$$, and $$g'$$ may form a commutative square. Let's focus on concurrent categories with that property.2 [2 Perhaps I should call them commutative categories? No, that would be confusing.]

Clearly all categories with pushouts form a canonical concurrent category, where the functor $$T$$ is the pushout functor. But concurrent categories can also have other structures. For example, consider the category $$N_+$$, where objects are natural numbers and arrows point from smaller to bigger numbers. This category has a unique pushout: $$b +_a c = \max \{b, c\}$$. However, there is an alternative way to make $$N_+$$ a concurrent category: if $$f : a \to b$$ and $$g : a \to c$$, we can define $$T(g, f) : c \to b + c$$ and $$T(f, g) : b \to b + c$$. Thus, a category with a unique pushout might have multiple concurrent structures on it.

Concurrent categories correspond naturally to the operational transform, which is all about defining functions $$f'$$ and $$g'$$ such that $$(g' \circ f)(x) = (f' \circ g)(x)$$. Additionally, the category-theoretic nature of concurrent categories automatically ensures that this operational transformation function respects composition and associativity, and it also automatically gives a rather subtle but important property that transporting some third function $$h$$ over either $$f g'$$ or $$g f'$$ should yield the same result.3 [3 A property whose importance was first formalized by M. Ressel, D. Nitsche-Ruhland, and R. Gunzenhäuser.]

## Concurrent functors

In the last post, my focus was on pushout-preserving functors. The analog for concurrent categories is what I call concurrent functors. A concurrent functor between concurrent categories $$(C, T)$$ and $$(D, S)$$, is a functor $$F : C \to D$$ that preserves the concurrent structure added by $$T$$, in other words where for any $$f$$ and $$g$$, $$F(T(f, g)) = S(F(f))(F(g))$$. This can be more easily expressed by noticing that $$F$$ provides a canonical map $$a / C \to F(a) / D$$; if we call that map $$F'$$, we require that $$T F' = F S$$.4 [4 This definitely looks suggestive!] Concurrent functors also have an analog of the natural transformation. In a normal natural transformation $$\alpha : F \to G : C \to D$$,5 [5 This is a home-grown notation of mine that I quite like.] we require that $$F(f) α_b = α_a G(f)$$. A concurrent natural transformation requires the same, but additionally requires that that commutative square is the square formed by the concurrent action in $$D$$: $$α_b = T(F(f), α_a)$$.

What is amazing about concurrent functors is that they share the properties I proved in my last post about pushouts: if $$(C, T)$$ and $$(D, S)$$ are concurrent categories, then so are the product $$(C, T) \times (D, S)$$ and concurrent functor $$(C, T) \to (D, S)$$ categories on them.6 [6 Proof omitted but not hard.]

These two facts together mean that concurrent categories, which are the natural way to talk categorically about the operational transform, can also interpret simply typed lambda calculus; that is, they can also be used to write programs.

## Footnotes:

1

2

Perhaps I should call them commutative categories? No, that would be confusing.

3

A property whose importance was first formalized by M. Ressel, D. Nitsche-Ruhland, and R. Gunzenhäuser.

4

This definitely looks suggestive!

5

This is a home-grown notation of mine that I quite like.

6

Proof omitted but not hard.