July 11, 2026

Tambara Equipment

Posted by Bartosz Milewski under Category Theory, Double category | Tags: , , , , , |
[2] Comments 

I was originally attracted to category theory when trying to understand Haskell optics. I was puzzled by the van Laarhoven’s functor representations and Kmett’s use of Tambara modules. By playing Tetris with the Yoneda lemma I was able to make some progress, attacking more and more esoteric topics. With a group of researcher and students at the Oxford Adjoint School in Applied Category Theory we cracked the problem of traversal optics and published a paper summarizing the advances in profunctor optics.

Optics sit at an intersection of monoidal actions and Tambara modules. There is a duality between optics and Tambara representations. It is related to what mathematicians call Tannakian reconstruction, when an algebraic object is recovered from the totality of its representations.

No wonder then that a recent article by Mateusz Stroiński, Module categories, internal bimodules and Tambara modules, piqued my interest. It turns out that Tambara modules can be thought of as horizontal arrows in a double category, which is also a proarrow equipment. I will try to sketch the contents of this paper and illustrate it using Haskell code.

The slogan is that Tambara modules are to monoidal functors as profunctors are to functors.

The main advantage of the double-categorical setting for Tambara modules is that it works out of the box for enriched categories.

Monoidal functors redux

For simplicity, I’ll be using a simplified version of a strict monoidal functor, which omits the object constraint from the definition of a monoidal category:

class (Actegory ten act1, Actegory ten act2, Functor f) =>
  MonFunctor ten act1 act2 f where
    alpha  :: m `act2` f a -> f (m `act1` a)
    alpha' :: f (m `act1` a) -> m `act2` f a

Here, alpha' is the inverse of alpha.

Monoidal functors compose:

newtype MonFunCompose f g a = 
  MonFunCompose { getMonFunCompose :: f (g a) }

and the composition is again a monoidal functor:

instance ( Actegory ten act1
         , Actegory ten act2
         , Actegory ten act3
         , MonFunctor ten act2 act3 f
         , MonFunctor ten act1 act2 g) 
        => MonFunctor ten act1 act3 (MonFunCompose f g)
  where
    alpha mfga = 
        let m3fga' = second getMonFunCompose mfga
            fmga = alpha @ten @act2 @act3 m3fga'
            fgma = fmap (alpha @ten @act1 @act2) fmga
        in MonFunCompose fgma
    alpha' (MonFunCompose fgma) = 
        let fmga = fmap (alpha' @ten @act1 @act2) fgma
            mfga = alpha'  @ten @act2 @act3 fmga 
        in  second MonFunCompose mfga

Notice the use of type application to help the Haskell type checker.

Tambara modules

A Tambara module is a profunctor that is compatible with the action of a monoidal category. If you interpret a profunctor as a proof-relevant relation, a Tambara module has the property that, whenever two objects are related, they remain related when you “multiply” them by the same object m. Multiplication in this case means the action of a monoidal category \mathbf M. In other words, a Tambara module is a profunctor J \colon A^{op} \times B \to \mathbf{Set} equipped with the transformation:

\lambda_{m a b} \colon J a b \to J (m \triangleright_1 a) (m \triangleright_2 b)

that is natural in a and b, and dinatural in m. The action interacts nicely with the monoidal structure:

\lambda_{(m \otimes n) a b} = \lambda_{m (n \triangleright a) (n \triangleright b)} \circ \lambda_{n a b}

\lambda_{1 a b} = id

(modulo some associators and unitors).

We can illustrate this in Haskell as a typeclass:

class (Actegory ten act, Profunctor j) 
  => Tambara ten act j where
    leftAct :: j a b -> j (m `act` a) (m `act` b)

I chose to concentrate on the left action of the actegory, but it’s easy to define the right action, or both. For simplicity, I’m using the same action for both arguments. In full generality, we would have two separate actegories.

The simplest example of a Tambara module is the hom-functor:

instance (Actegory ten act) => Tambara ten act (->) where
    leftAct :: Actegory ten act => (a -> b) -> m `act` a -> m `act` b
    leftAct = second

Here I used the bifunctoriality of the action.

Tambara modules form a category, in which action-preserving natural transformations act as morphisms.

The usual profunctor composition using coends also works on Tambara modules.

data TamCompose p q d c where
  TamCompose :: p x c -> q d x -> TamCompose p q d c

The result of composition is again a Tambara module:

instance (Tambara ten act p, Tambara ten act q) 
  => Tambara ten act (TamCompose p q) where
    leftAct :: (Tambara ten act p, Tambara ten act q) =>
        TamCompose p q a b -> TamCompose p q (m `act` a) (m `act` b)
    leftAct (TamCompose pxc qdx) 
      = TamCompose (leftAct pxc) (leftAct qdx)

Taken together, we have a bicategory \mathbf{Tam}, where actegories are 0-cells, Tambara modules with coend composition are 1-cells, and natural transformations between them are 2-cells.

Moreover, endo-Tambara modules, that is Tambara modules that operate within a single category, form a monoidal bicategory, with profunctor composition acting as a tensor product and a hom-functor acting as a unit.

Tambara Equipment

We have previously studied a double category \mathbb{P}rof in which categories are 0-cells, profunctors are horizontal arrows, functors are vertical arrows, and natural transformations form 2-cells. This double category happens to be a proarrow equipment, which relates functors to representable profunctors in a specific way.

It turns out that there is an analogous construction with actegories as 0-cells, Tambara modules as horizontal 1-cells, and monoidal functors as vertical 1-cells. To form 2-cells, we first have to be able to lift (or restrict) a Tambara module along a pair of monoidal functors. We define a lifting of J as the profunctor:

\langle a, c \rangle \mapsto J(f a)(g c)

or, using placeholders, J(f -) (g =). In Haskell this is:

newtype Lift f g j a c = Lift (j (f a) (g c))

The lifting of a Tambara module is again a Tambara module with the structure map defined as a composition:

J (f a) (g c) \xrightarrow{\lambda_{m (f a) (g c)}} J (m \triangleright_2 f a) (m \triangleright_2 g c) \xrightarrow {J \alpha^{-1} \alpha} J (f (m \triangleright_1 a)) (g (m \triangleright_1 c))

The second arrow lifts the (invertible) monoidal functor structure map to J:

\alpha \colon m \triangleright_2 g c \to g (m \triangleright_1 c)

Here’s the same thing in Haskell:

instance ( Actegory ten act1
         , Actegory ten act2
         , MonFunctor ten act1 act2 f
         , MonFunctor ten act1 act2 g
         , Tambara ten act2 j) 
    => Tambara ten act1 (Lift f g j) where
    leftAct (Lift j) = Lift $ dimap alpha' alpha $ leftAct @ten @act2 j

I used type applications to select the correct left action corresponding to act2.

A 2-cell is then a natural transformation from H to the lifting of J.

Or, in Haskell:

type Cell f g h j = forall a c . h a c -> j (f a) (g c)

The companion and the conjoint are representable profunctors, that are automatically Tambara modules as long as f is a monoidal functor (the Identity functor is trivially monoidal):

type Companion f d c = Lift f Identity (->)
type Conjoint f d c  = Lift Identity f (->)

The unit and counit cells for the companion and the conjoint are reasonably easy to define (see the linked code).

Free Tambara and Optics

There is an obvious forgetful functor from \mathbf{Tamb} to \mathbf{Prof} (it forgets the action). This functor has a left adjoint. For any profunctor J, it produces a free Tambara module given by the following coend:

(\Phi J) \, s t = \int^m \int^{x y} C(s, m \triangleright x) \times J x y \times C(m \triangleright y, t)

In Haskell, we model it as an existential data type:

data FreeTamb ten act j s t = 
  forall m x y. (MonoidalCategory ten, Actegory ten act) 
  => FreeTamb (s -> m `act` x) (j x y) (m `act` y -> t)

The result is indeed a Tambara module:

instance (Actegory ten act, MonoidalCategory ten, Profunctor j) 
  => Tambara ten act (FreeTamb ten act j) where
    -- na -> (nm)c, jcd, (nm)d -> nb
    leftAct (FreeTamb a_mc jcd md_b) = FreeTamb f jcd g
      where
        --f :: n `act` a -> (n `ten` m) `act` c
        f  na = assoc' $ second a_mc na
        --g :: (n `ten` m) `act` d -> n `act` b
        g nm_d= second md_b $ assoc nm_d

It so happens that optics can be defined as a free Tambara module acting on a representable profunctor \Theta_{a b} x y = C(x, a) \times C(b, y). Indeed, applying the Yoneda reduction, we get:

O\, s t a b = \int^{m} C(s, m \triangleright a) \times C(m \triangleright b, t)

In Haskell

data Rep a b x y = Rep (x -> a) (b -> y)

giving us:

type Optic ten s t a b = FreeTamb ten (Rep a b) s t

which, by Yoneda reduction, is isomorphic to:

data Optic ten act s t a b = forall m.
    Optic (s -> m `act` a) (m `act` b -> t)

Internalizing monoidal actions

A monoidal action, seen as a functor \mathbf M \to [C, C], can be internalized in M if it has a right adjoint:

C(m \triangleright a, t) \cong \mathbf M (m, \{a, t \} )

If you think of the action as “multiplication,” the adjunction is reminiscent of currying, and the right adjoint plays to role on the “internal hom.”

In Haskell, we define a typeclass:

class (Actegory ten act, MonoidalCategory ten, Profunctor hom) 
  => IntHom ten act hom | hom -> act where
    icurry   :: (m `act` a -> b) -> (m -> hom a b)
    iuncurry :: (m -> hom a b)   -> (m `act` a -> b)

We can use this adjunction to simplify multiplicative optics:

\int^{m} C(s, m \triangleright a) \times C(m \triangleright b, t) \cong \int^{m} C(s, m \triangleright a) \times \mathbf M (m, \{b, t \})

Using the Yoneda reduction (a.k.a, “integrating” over m), this is equivalent to:

O \, s t a b \cong C(s, \{b, t \} \triangleright a )

With additive optics, we use the right adjoint to coproduct to produce hom-sets in a product category.

Both tricks are used in simplifying traversals, which are optics generated by polynomial functors:

\int^{c \colon [\mathbb N , Set]} C(s, \sum_n c_n \times a^n) \times C (\sum_m c_m \times b^m, t)

Here, c is a natural-number-indexed family of objects with a monoidal structure given by convolution; and a^n and b^n are powers.

We first use the coproduct adjunction:

C (\sum_m c_m \times b^m, t) \cong \prod_m C(c_m \times b^m, t)

and follow it by the currying adjunction. We get the formula for a traversal:

T \, s t a b \cong Set(s, \sum_n Set(b^n, t) \times a^n)

The result can be illustrated in Haskell by replacing powers with lists:

type Traversal s t a b = s -> ([b] -> t, [a])

Internal monoid

The endo-hom \{a, a\} is automatically a monoid in \mathbf M. Indeed, we can define monoid multiplication as:

\mathbf M(\{a, a\} \otimes \{a, a\}, \{a, a\}) \cong C\big((\{a, a\} \otimes \{a, a\}) \triangleright a, a\big)

The right hand side can be implemented as a double application of the counit of the adjunction:

\epsilon_{a a} = \{a, a\} \triangleright a \to a

In Haskell, we first define a monoid internal to a monoidal category:

class (MonoidalCategory ten) => IMonoid ten m where
    imempty  :: Unit ten -> m
    imappend :: m `ten` m -> m

and show that hom a a is an instance of it:

instance (Actegory ten act, MonoidalCategory ten, IntHom ten act hom)  
  => IMonoid ten (hom a a) where
    imempty = icurry unit
    -- imappend :: (hom a a) `ten` (hom a a) -> hom a a
    imappend = icurry (eval . second eval . assoc)

where counit of the adjunction is the eval function:

eval :: (Actegory ten act, MonoidalCategory ten, IntHom ten act hom) 
  => hom a b `act` a -> b
eval = iuncurry id

Haskell code for this blog post is available here.

 

May 18, 2026

Bending, Yanking, and Cartesian Squares in Double Categories

Posted by Bartosz Milewski under Category Theory | Tags: , , , , , |
Leave a Comment 

Previously: Profunctor Equipment in Haskell.

The major advantage of string diagrams is that they provide surprisingly natural language for complex diagram manipulations. The fact that two traditional diagrams are equal can be often described as a permission to bend, yank, or pinch strings in particular ways. They provide visual and often tactile clues to our senses. This is even more helpful in the context of double categories and equipments.

Yanking

Consider the definition of a companion from the previous installment. It’s a horizontal arrow B(f, 1) that is somehow related to a vertical arrow f \colon A \to B. There are two 2-cells that illustrate this relation, but it’s not clear what their meaning is or how to use them.

It’s only when you start composing these cells that the computational aspect of companions emerges. The first condition is that the horizontal composite result in the identity \eta \epsilon = id_f. Diagrammatically, we have:

You can visualize this as yanking the ends of the two arrows and letting the beads fall down.

The same trick can be done with vertical composition. The equation, \epsilon \odot \eta = id_{B(1, f)}, is illustrated by the following diagrams:

This time we yank the arrows horizontally.

The two equalites for the conjoint arrows have analogous graphical interpretation resulting it this general rule that is valid in any proarrow equipment:

Any zig-zag in which the arrows flow in one direction and vertical arrows point downwards can be yanked.

The Spider Lemma

The yanking identities let us prove a very powerful lemma, which lets us bend arrows in many diagrams. The so called spider lemma states that the two diagrams below are isomorphic.

To prove it, we fist etablish two mappings: To get from the left diagram to the right one, we top it (vertically precompose) with the unit of the conjoint and the unit of the companion. This bends the arrows f_1 and f_3 and turns them into A_1(1, f_1) and A_3(f_3, 1). Then we shove the two counits below it (vertically postcompose), to bend the arrows g_1 and g_3.

To get from the right diagram to the left one, we do the analogous trick with horizontal pre/post composition. Finally, we prove that the two mappings are the inverse of each other by composing them and applying the yanking identities.

This is the spider lemma in its full glory, but we often specialize it to situations when one or more vertical arrows are identities. Then it lets us bend the remaining arrows.

Cartesian Squares

The workhorse of category theory is the universal construction. You define a new gadget by specifying its shape, and then pick the one through which all those shapes uniquely factor through. This is, for instance, how a categorical product is defined: The shape is a span with two fixed objects at its ends and a central object with arrows towards those objects. The product is the span through which all other spans factor through.

The same idea works in a double category, except that now we want to view it through string diagrams. We’ll illustrate it with the definition of a cartesian square.

Given a horizontal arrow J and two vertical arrows f and g, a cartesian square defines a horizontal arrow H = J(f, g) also called a restriction of J along f and g. In the profunctor equipment \mathbb{P}rof, this restriction is given by the hom-functor:

\langle a, c \rangle \mapsto J(f a, g c)

Since we want to avoid mentioning hom-sets, we’ll use a universal construction instead. Here’s the shape we are going to study:

We are given four 0-cells (the four areas), two vertical 1-cells f and g, and one horizontal cell J. We want to find the universal one of H and \alpha. To this end we replace H with a generic horizontal arrow L \colon X \to Y, together with two new vertical arrows h and k that, just like H and \alpha before, are equipped with a 2-cell \psi (see the left diagram below).

The universal condition states that any such shape can be uniquely factored out through the cartesian square \alpha (see the right diagram below).

Visually, we are splitting the bead representing \psi into two separate beads, the right one being the universal one. Or you may interpret it, right to left, as pinching together the two beads into one.

Most universal constructions in a double category look like this. You may easily figure out the definition of the opcartesian square by extending it on the right instead of on the left.

In \mathbb{P}rof, this universal condition is a tautology, but in other double categories it may have computational meaning. It can be used, for instance, to compute a 2-cell \psi' from L to J(f, g) over a pair of 1-cells (h, k), given the corresponding cartesian square \alpha. All we need is to find a suitable \psi from L to J over the composite (f \circ h, g \circ k).

 

April 24, 2026

Profunctor Equipment

Posted by Bartosz Milewski under Category Theory | Tags: , , , , , , |
1 Comment 

The fundamental premise of category theory is that it’s possible to fully capture the nature of objects by describing their interactions with other objects of the same type. Those interactions are encoded using morphisms: arrows between objects.

What about categories themselves? We define a category by describing its internals: objects and arrows. But true to the categorical credo, we should be able to capture the essence of a category by describing its interactions with other categories. (Small) categories are objects in the category of categories Cat, with functors as morphisms.

In fact Cat has even more structure: functors between any two categories form a functor category, with natural transformations as morphisms. This makes Cat a 2-category, with categories as 0-cells, functors as 1-cells, and natural transformations as 2-cells.

With this much structure, we can define a lot of categorical constructions. In particular, we can define adjunctions as pairs of functors equipped with the unit and counit natural transformations. We can also define monads as endofunctors equipped with the unit and multiplication natural transformations, and so on.

However, there are some categorical constructions that force us to look at the internals of categories. In particular, anything that involves representable functors cannot be defined without talking about hom-sets, which are internal to categories. In particular there are things like (weighted) limits or pointwise Kan extensions that rely on representability.

We somehow need to incorporate the information about hom-sets into the fabric of of the 2-category Cat. At the minimum, we need to identify the hom-functors:

C(-, =) \colon C^{op} \times C \to Set

Such functors of mixed variance are called profunctors and, in general, they can go between different categories, as in P \colon C^{op} \times D \to Set. In fact, profunctors can be considered arrows in the category Prof. Not only that, Prof is itself a bicategory, whose 0-cells are (small) categories, 1-cells are profunctors, and 2-cells are natural transformations between profunctors. Composition of profunctors is defined using the coend formula:

(P \odot Q)\langle c, e \rangle = \int^{d \colon D} P \langle c, d \rangle \times Q \langle d, e \rangle

What is important is that the hom-functor C(-, =) is the identity profunctor with respect to this composition. It means that we have a way of talking about hom-sets and representables without peeking inside individual categories.

The usual categorical laws, associativity and identity, are only satisfied up to isomorphism (that is up to invertible 2-cells), hence Prof is called a bicategory and not a 2-category, whose laws are satisfied on the nose.

These two categories, the 2-category Cat and the bicategory Prof can be combined into a single double category, which we’ll call \mathbb{P}rof. The 0-cells are the usual categories; but now we have two kinds of arrows: the vertical ones are functors, and the horizontal ones are profunctors. What glues them together are the 2-cells.

Here’s a 2-cell that combines two (vertical) functors f \colon A \to B and g \colon C \to D with two (horizontal) profunctors H \colon A \to C and J \colon B \to D.

In our double category \mathbb{P}rof, this 2-cell is implemented as a natural transformation, whose component at the pair of objects \langle a, c \rangle is a function:

\alpha_{\langle a, c \rangle} \colon H \langle a, c \rangle \to J \langle f a, g c \rangle

It’s a member of the set of natural transformations, which can be written as an end:

\int_{a c} Set(H \langle a, c \rangle, J \langle f a, g c \rangle)

The profunctor J \langle f a, g c \rangle is sometimes called the restriction of J along f and g.

In an abstract double category, a 2-cell is just something that says that the particular four arrows in this configuration are related.

The same diagram can be transformed into a string diagram. Here, the 0-cells are the four areas, 1-cells form boundaries between those areas, and a 2-cell is a node connecting the four subdivisions:

We encode identity 1-cells in string diagrams by simply omitting the corresponding lines/arrows.

2-cells can be composed both horizontally and vertically by gluing them along identical edges.

In \mathbb{P}rof, horizontal composition of 2-cells corresponds to the (vertical) composition of natural transformations between profunctors (we’ll write this composition as a juxtaposition, as in \alpha \beta, in diagram order).

The identity 2-cell at a profunctor P is just an identity natural transformation:

Vertical gluing of string diagrams results is a natural transformation between composite profunctors. For instance this diagram:

is a composition of two natural transformation:

\alpha_{\langle a, c \rangle} \colon P \langle a, c \rangle \to R \langle f a, g c \rangle
\beta_{\langle c, e \rangle} \colon Q \langle c, e \rangle \to S \langle g c, h e \rangle

whose component is a function:

(\beta \odot \alpha)_{\langle a, e \rangle} \colon \int^c P\langle a, c \rangle \times Q \langle c, e \rangle \to \int^{c'} R \langle f a, g c' \rangle \times S \langle g c', h e \rangle

By co-continuity of the coend, this is isomorphic to:

\int_c \big(P\langle a, c \rangle \times Q \langle c, e \rangle \to \int^{c'} R \langle f a, g c' \rangle \times S \langle g c', h e \rangle \big)

and is implemented by composing the product \alpha_{\langle a, c \rangle} \times \beta_{\langle c, e \rangle} with the appropriate injection into the coend.

The unit of vertical composition at a functor f in \mathbb{P}rof is a 2-cell:

which is a natural transformation A(a, a') \to B(f a, f a') implementing the functoriality of f.

Companion and Conjoint

Given a functor f \colon A \to B we can construct two representable profunctors, the companion and the conjoint.

The companion is denoted by B(f, 1) or f_*. In \mathbb{P}rof, it is the profunctor generated by the following hom-functor:

\langle a, b \rangle \mapsto B (f a, b )

A conjoint, which is denoted by B(1, f) or f^*, is defined in \mathbb{P}rof as:

\langle b, a \rangle \mapsto B (b, f a)

Notice that these two horizontal arrows go in opposite directions. The companion goes from A to B (the same as f), and the conjoint goes from B to A. Later we’ll see that they form an adjunction.

In these definitions we have used the hom-sets explicitly, something we were trying to avoid. We should therefore try to define the companions and the conjoints abstractly by listing their properties.

Companion


In a string diagram, the companion of a vertical arrow f \colon A \to B is represented by a left-pointing horizontal arrow:

It is equipped with two 2-cells called the unit and the counit (the subscript p stands for comPanion):

Indeed, using the rules for reading string diagrams in \mathbb{P}rof, the unit corresponds to a natural transformation:

\eta_{\langle a, a' \rangle} \colon A (a, a') \to B (f a, f a' )

which just expresses the functoriality of f. The (invisible) horizontal line on the left stands for the identity profunctor A(a, a').

The counit in \mathbb{P}rof:

\epsilon_{\langle a, b \rangle} \colon B (f a, b) \to B (f a, b)

is trivially instantiated by the identity natural transformation.

There are two ways we can compose these two 2-cells. Both of them should result in some kind of identities. For instance, this is the horizontal composition:

\eta \epsilon = id_f

where id_f is the identity at f which, in \mathbb{P}rof is a functorial action of f on the hom-set.

Similarly, vertical composition gives us:

\epsilon \odot \eta = id_{B(f, 1)}

Conjoint

The conjoint of f \colon A \to B is represented by the right-pointing horizontal arrow:

In \mathbb{P}rof, the conjoint is the representable profunctor: \langle b, b' \rangle \mapsto B(b, f b')

The conjoint is related to the original functor by its unit and counit 2-cells:

(here, the subscript j stands for conJoint). Their two compositions produce identity 2-cells:

\eta \epsilon = id_f
\eta \odot \epsilon = id_{B(1, f)}

Adjunction

We can also compose units with units and counits with counits by connecting the functor arrows:

These diagrams can be interpreted as the unit and counit of the adjunction B(1, f) \dashv B(f, 1):

\eta \colon id_A \to B(f, 1) \odot B(1, f)

\epsilon \colon B(1, f) \odot B(f, 1) \to id_B

In Prof, the profunctor composition is given by the coend, so we get, for the unit:

\eta \colon A(a, a') \to \int^b B(f a, b) \times B(b, f a')

We use the Yoneda reduction to eliminate the coend:

\int^b B(f a, b) \times B(b, f a') \cong B(f a, f a')

The unit is then instantiated by the functoriality of f.

The counit is:

\int^a B(b, f a) \times B(fa, b') \to B(b, b')

By co-continuity of the coend, this is isomorphic to:

\int_a \big(B(b, f a) \times B(fa, b') \to B(b, b')\big)

which is inhabited by the composition of hom-sets.

The Big Picture

We’ve seen how to combine the 2-category Cat with the bicategory Prof into one double category \mathbb{P}rof. In this double category every vertical arrow has a horizontal companion and every companion has a conjoint. A double category with this kind of structure is called a proarrow equipment. It has just enough structure to define abstractly such categorical constructions as weighted limits or pointwise Kan extensions. We can then apply those constructions to other double categories, without having to repeat ourselves.

One immediate application is to enriched categories and enriched profunctors, which form a proarrow equipment \mathbb{V}\text{-Cat}. Or we can consider a simpler case of the double category of sets and relations. We can also add more structure to the categories in question, for instance by considering monoidal categories; or even go meta, and study the double category of (weak) double categories \mathbb{D}bl.