Bartosz Milewski's Programming Cafe

November 10, 2026

Twisted Optics

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

A general optic can be defined as a set of bidirectional transformations:

$O(s, s')(a, a') = \int^{m \colon M} C(s, m \triangleright a) \times D(m \blacktriangleright a', s')$

It is buit from two actegories, $C$ and $D$ ; each with its own monoidal action by a monoidal category $M$ (the two actions are represented by two different triangles).

A product of two hom-sets may be interpreted as a hom-set in a product category. The reversal of one of the hom-set may be accomplished by invoking the opposite category.

If we use $\underline s$ for a pair of objects $(s, s')$ in $C \times D^{op}$ , and $\underline a$ for $(a, a')$ , we may want to encode such an optic as:

$O \underline s \; \underline a = \int^m (C \times D^{op})( \underline s, m \triangleright \underline a)$

with the action $m \triangleright \underline a = (m \triangleright a, m \blacktriangleright a')$ .

This is a slight abuse of notation. Normally, a coend variable $m$ should occur in the integrand twice; once in a covariant and once in a contravariant position. To justify this new notation, let’s dig deeper into the definition of a coend.

A coend $\int^m P (m, m)$ is a giant sum over all the the sets formed by taking the diagonal elements of the profunctor $P$ — modulo certain identifications. These identifications are crucial, because they probe the structure of the categories in question; they tell us that we are overcounting certain set elements because they are reachable through underlying morphisms.

The identification is done through cowedges. A cowedge with a vertex $V$ is a family of morphisms (injections) $\iota_m \colon P (m, m) \to V$ such that for any morphism $f \colon m \to n$ the following diagram commutes:

We read the commuting condition as:

$\iota_m \circ P(f, m) = \iota_n \circ P(n, f)$

In a sum (disjoint union) of all these sets $P(m, m)$ , we identify the elements that can be reached through such composites. One composite contains the lifting of the pair $(f, id_m)$ ; and the other, the lifting of $(id_n, f)$ .

Cowedges form a category, and the terminal cowedge for a given profunctor is called the coend.

Twisted Arrow Category

A giant sum with identifications can also be described as a colimit, if we can find the appropriate category to define the cocones. We will want to match cocones with cowedges.

Each cowedge corresponds to a family of injections $\iota_m$ and an arrow $f$ in $M$ . This suggests that the appropriate category for constructing the colimit is the category of arrows. An object is this category is an arrow $f \colon m \to n$ or, more precisely, a triple $(m, n, f)$ .

The tricky part is to define morphisms between arrows. Since we are working with profunctors, it makes sense to define a morphism between $(m, n, f)$ and $(m', n', f')$ as a pair of arrows going in opposite directions:

$(u \colon m' \to m, v \colon n \to n')$

More precisely, a morphism between arrows is a pair of morphisms $(u, v)$ satisfying the commuting condition $f' = v \circ f \circ u$ :

(Incidentally, without this commuting condition, all arrows between a fixed pair of objects would be isomorphic.)

Such a category is called a twisted-arrow category $\mathbf{Tw}(M)$ .

It can be shown that an end of a profunctor is isomorphic to a limit over $\mathbf{Tw}(M)$ .

Here we are interested in a coend, so we’ll have to slightly modify the proof. We’ll show that a coend is isomorphic to a colimit over the opposite catoegory $\mathbf{Tw}^{op}(M^{op})$ . An object in this category is a triple $(n, m, f \colon m \to n)$ , in which the direction of the arrow is reversed. Morphisms are similarly reversed:

$(n, m, f) \xleftarrow{(u, v)} (n', m', f')$

They satisfy the commuting condition:

Cocones

A colimit is defined in terms of cocones. A cocone with a vertex $V$ is a functor:

$G \colon \mathbf{Tw}^{op}(M^{op}) \to \mathbf{Set}$

together with a family of injections:

$\tau_f \colon G (n, m, f) \to V$ .

Let’s define the functor $G$ using our profunctor $P$ . On objects, we have the obvious candidate:

$G (m, n, f) = P (m, n)$

The tricky part is to define the action of $G$ on morphisms. The image, under $G$ , of a morphism $(u, v)$ is a function between sets:

$G(u, v) \colon G(n', m', f') \to G (n, m, f)$

We define it as:

$G (u, v) = P (v, u)$

The action of $G$ is illustrated in this picture:

From Cocones to Cowedges

We can now establish a one-to-one correspondence between cocones and cowedges.

First of all, a cocone with a vertex $V$ is built from a family of injections:

$\tau_f \colon G(n, m, f) \to V$

It’s easy to build the diagonal injections, coming from $G (m, m, id_m)$ . We make them equal to the cowedge injections:

$\tau_{id_m} = \iota_m$

A general injection $\tau_f \colon G (n, m, f) \to V$ is given by either of the two formulas:

$\tau_f = \iota_m \circ P (f, m) = \iota_n \circ P n f$

which are equal by the wedge condition. This is illustrated by the following diagram:

Next we have to show that the triangles forming the sides of the cocone commute. Here’s one of such triangles:

The trick is to factorize the top morphism:

$(n', m', f') \xrightarrow{(m', v)} (n, m', g) \xrightarrow{(u, n)} (n, m, f)$

where $g = f \circ u$ . Here, the identity morphisms are written as their corresponding objects, $(m', v) = (id_{m'}, v)$ , etc. This decomposition is illustrated in the following diagram:

Keep in mind the commuting condition in the definition of a twisted morphism:

$f' = v \circ f \circ u = v \circ g$

We can now factorize the top arrow of our triangle as follows:

$G(n', m', f') \xrightarrow{ G(m', v)} G(n, m', g) \xrightarrow{G(u, n)} G(n, m, f)$

We then decompose our triangle into a pair of triangles and the diamond. Translating between the functor $G$ and the profunctor $P$ , we build the following diagram:

The two triangles commute by functoriality, and the diamond is the cowedge for $P$ . The mapping goes both ways: given a cocone $(G, \tau)$ we can reconstruct the cowedge.

Finally, just like cowedges form a category, so do cocones; and we have just sketched the equivalence of the two categories. It follows that the terminal objects in the two categories are equivalent, therefore coends are isomorphic to colimits.

Twisted Optics

We can now give a precise meaning to the shorthand notation for optics:

$O \underline s \; \underline a = \int^m (C \times D^{op})( \underline s, m \triangleright \underline a)$

This is a colimit over the appropriate twisted arrow category:

$O \, \underline s \; \underline a = \text{colim}_{m \colon \mathbf{Tw}^{op}(M^{op})} (C \times D^{op})( \underline s, m \triangleright \underline a)$

The advantage of this definition is that it can be generalized to a double-categorical setting, where colimits have a precise meaning.

If you want to learn more about ends and coends, I recommend reading Coend Calculus by Fosco Loregian.

September 21, 2026

Tannakian Reconstruction in a Yoneda Equipment

Posted by Bartosz Milewski under Category Theory, Profunctor Equipment | Tags: Category Theory, Proarrow Equipment, Tannaka |
Leave a Comment

The reason I bored you with the Yoneda equipment was to eventually double back to Tannakian reconstruction.

In a nutshell, Tannakian reconstruction lets us reconstruct the hom-set from a set of natural transformations between fiber functors:

$\int_{\hat F \colon \hat A} \mathbf{Set}( \hat F a, \hat F b) \cong A(b, a)$

Here, the end goes over the presheaf category.

We have previously learned that we can define a presheaf object in a double category, together with the evaluation functor $E$ that works exactly like the fiber functor:

$E \langle a, \hat F \rangle = \hat F a$

In an equipment, we can define it as a companion to the Yoneda functor:

$E = y_*$

Furthermore, in a Yoneda equipment, as a generalization of full-faithfullness, we postulate that the unit of the adjunction:

$y^* \dashv y_*$

is an isomorhpism:

$1 \cong y_* \odot y^*$

The only missing piece of the puzzle is to realize that the end in the Tannakian formula is the right Kan lift.

Right Kan Lift

The right Kan Lift is defined as the right adjoint to postcomposition. This definition is easy to interpret when only functors are involved, because postcomposition is well defined: Postcomposing with $f$ is a mapping:

$g \mapsto f \circ g$

so the right lift is defined as:

$(f \circ -) \dashv \text{Rift}_f$

The order of composition of profunctors is more convention-dependent, and the convention I used was for diagram-order composition, which happens to be the opposite of functor composition.

Thus, in $\mathbb{P}rof$ , we’ll expand the adjunction to the following isomorphism of natural transformations between profunctors:

$(S \odot P \Rightarrow Q) \cong (S \Rightarrow \text{Rift}_P Q)$

In components, the left hand side is a double end:

$\int_{a, c} (S \odot P) \langle a, c \rangle \to Q\langle a, c \rangle$

Expanding the profunctor composition, we get:

$\int_{a, c} \big( \int^b S \langle a, b \rangle \times P \langle b, c \rangle \big) \to Q \langle a, c \rangle$

Using co-continuity, we can pull the coend out:

$\int_{a, c, b} \big( S \langle a, b \rangle \times P \langle b, c \rangle \to Q \langle a, c \rangle \big)$

We then curry the product:

$\int_{a, c, b} \big( S \langle a, b \rangle \to (P \langle b, c \rangle \to Q \langle a, c \rangle ) \big)$

and re-arrange the ends:

$\int_{a, b} \big( S \langle a, b \rangle \to (\int_c P \langle b, c \rangle \to Q \langle a, c \rangle ) \big)$

We conclude that the right Kan lift is given by the formula:

$(\text{Rift}_P Q) \langle a, b \rangle = \int_c (P \langle b, c \rangle \to Q \langle a, c \rangle )$

What we did is a pretty standard calculation of a mapping out of a profunctor composition. We pull out the coend to turn it into an end, and then we curry the product.

A right Kan lift can be defined in a double category (actually, all we need is the horizontal=bicategorical part of it) using the counit 2-cell:

satisfying the universal property: Any 2-cell of the same shape as the counit uniquely factorizes through the counit:

Tannakian Reconstruction

We can now see that, in $\mathbb{P}rof$ , the left hand side of the Tannakian formula is the right Kan lift of the evaluation profunctor along itself:

$(\text{Rift}_E E) \langle b, a \rangle = \int_{\hat F \colon \hat A} \mathbf{Set}( E \langle a, \hat F \rangle, E \langle b, \hat F \rangle) \cong \int_{\hat F \colon \hat A} \mathbf{Set}( \hat F a, \hat F b)$

In a Yoneda equipment, the evaluation profunctor is the companion to the Yoneda functor, so we can replace $\text{Rift}_E E$ with $\text{Rift}_{y_*} y_*$ .

Using the definition of the Right Kan lift as a right adjoint to postcomposition we have, for any $S$ :

$(S \odot y_* \Rightarrow y_*) \cong (S \Rightarrow \text{Rift}_{y_*} y_*)$

In a proarrow equipment, the companion $y_*$ has a right adjoint, the conjoint $y^*$ . Graphically, this lets us bend the arrows in the diagram:

We get:

$(S \Rightarrow \text{Rift}_{y_*} y_*) \cong (S \odot y_* \Rightarrow y_*) \cong (S \Rightarrow {y_*} \odot y^*)$

Since $S$ is arbitrary, we can use the Yoneda lemma (the bicategorical version) to conclude that:

$\text{Rift}_{y_*} y_* \cong {y_*} \odot y^*$

Finally, in a Yoneda equipment we postulate the analog of the full-faithfullness of the Yoneda embedding:

$1 \cong y_* \odot y^*$

The Tannakian reconstruction in a Yoneda equipment can therefore be written as:

$\text{Rift}_{y_*} y_* \cong 1$

In a profunctor equipment, the unit on the right hand side is the hom-profunctor $A(b, a)$ .

September 13, 2026

Yoneda Lemma in Double Categories

Posted by Bartosz Milewski under Category Theory, Profunctor Equipment | Tags: Category Theory, Double Category, Proarrow Equipment, Profunctors, Yoneda Structure |
[2] Comments

Working with double categories can be aptly summarized in a meme: Talk to me about sets without mentioning sets. We don’t talk about hom-sets, we talk about horizontal units. Secretly, we are visualizing horizontal arrows as profunctors, and the unit of profunctor composition is a hom-functor.

Presheaves are defined as $\mathbf{Set}$ -valued functors, so we immediately run into a problem when trying to describe them in a double category. And without presheaves, we can’t talk about the Yoneda lemma — the workhorse of category theory.

Granted, a lot of standard categorical constructions can be generalized to use profunctors in place of presheaves, with immediate generalization to double categorical settings. This can be done with (weighted) limits, Kan extensions, categories of elements (tabulations), and many others. But sometimes you just need to talk about presheaves without mentioning presheaves.

I will first sketch the constructions in category theory and, in the next installment, show you a toy implementation in Haskell.

Overview

To translate the Yoneda construction into the language of double categories, we need to define an object (a 0-cell) $\hat A$ of presheaves and a Yoneda vertical arrow (1-cell) $y_A \colon A \to \hat A$ — the Yoneda embedding. We take our guidance from the category of presheaves $\hat A = [A, \mathbf{Set}]$ , where the Yoneda functor is defined as a representable functor:

$y_A a = A(-, a)$

Since in this picuture the 0-cells of a double category represent categories, with no access to their objects, we have to define everything using universal constructions.

Even the simplest thing, like the action of a presheaf on an object resulting in a set, has to be defined in bulk, as a particular horizontal arrow from $A$ to $\hat A$ .

We would also like the Yoneda embedding to be dense– a generalization of the slogan that every presheaf is a colimit of representables. We can express this in terms of left Kan extensions, which we know how to generalize to double categories.

Finally, we want the Yoneda embedding to be full and faithful, without talking about the mapping of hom-sets.

Most of this stuff can be expressed using 2-cells, which we can visualize using string diagrams. The problem is that a 2-cell translates into a one-way mapping, from left to right. What we often need is isomorphisms, which require some 2-cells to be invertible.

Classifying Arrows

It’s easy to turn a functor into a profunctor. In fact there are two canonical ways of defining representable profunctors. In a proarrow equipment they correspond to the companion and the conjoint, $C(1, f)$ and $C(f, 1)$ . But it’s also possible to build a functor from a profunctor.

The rough idea is that a profunctor:

$H \colon A^{op} \times B \to \mathbf{Set}$ .

when curried, can be seen as a functor into the presheaf category:

$f_H \colon B \to (A^{op} \to \mathbf{Set})$
$f_H b = H \langle -, b \rangle$

(Koudenburg calls this functor $H^{\lambda}$ ). I’ll use the notation $\hat A$ for the category of presheaves on $A$ , so we can write:

$f_H \colon B \to \hat A$

(In what follows, I’ll sometimes omit the subscript $H$ .)

In components, this equivalence can be written as an invertible natural transformation:

$\xi_{a b} \colon H \langle a, b \rangle \to (f_H b) \, a$

There is one more detail that requires special attention: $f_H b$ is an object in the category $\hat A$ . What does it mean to apply this object to $a$ ? We know what it means in $\mathbf{Cat}$ , where:

$\hat A = [C^{op}, \mathbf{Set}]$

is a functor category. We don’t think twice about applying functors to objects. But what it really means is that we are using the counit of the currying adjunction, the evaluation (pro-)functor:

$E \colon A^{op} \times \hat A \to \mathbf{Set}$

The currying of the profunctor $H$ can thus be written, in full generality, as:

$H \langle a, b \rangle \cong E \langle a, f_H b \rangle$

One direction, left to right, of this identity can be illustrated as a double-categorical 2-cell:

We get the other direction by requiring this square to be cartesian (see Appendix 1).

The pair $(\hat A , E)$ is sometimes called the classifier for $A$ . It lets us classify horizontal arrows $H$ using vertical arrows $f_H$ .

Yoneda Embedding

We can now ask the question: What is the classifying arrow for the simplest horizontal arrow: the unit arrow? In $\mathbb{P}rof$ , the unit arrow is the hom-profunctor $A(-, =)$ . Its classifying arrow is the functor $y_A \colon A \to \hat A$ . The 2-cell defining this classification:

evaluates to:

$A(x, a) \to E \langle x, y_A a \rangle$

or, expanding $E$ :

$A(x, a) \to (y_A a) x$

Compare this with the definition of the Yoneda embedding:

$y_A a = A(-, a)$

You may also recognize this 2-cell as a definition of the unit of a companion. Thus, in a proarrow equipment, the evaluation profunctor can be seen as a companion to the Yoneda functor:

$E = \hat A (y_A, 1)$

The terse notation for the companion of a functor $f$ is $f_*$ , so we ofter write (omitting the subscript $A$ ):

$E = y_* = \hat A (y, 1)$

With this definition of $E$ , and with the bending of the $y$ arrow, we can redraw the original diagram defining the currying of $H$ :

To generalize the condition that every presheaf is a colimit of representables, we want $y$ to be dense.

A functor is dense if its left Kan extension along itself (called the density comonad) is isomorphic to identity:

$\text{Lan}_{y_*} y \cong id_y$

The Adjunction

In a proarrow equipment, the counit of the companion is a 2-cell:

$E \langle a , \hat F \rangle \to \hat A ( y a, \hat F )$

with $\hat F$ an object (presheaf) in $\hat A$ and $E = y_*$ :

In $\mathbb{P}rof$ , this is:

$\hat F a \to [A, \mathbf{Set}](A(-, a), \hat F)$

Observe that this is half of the Yoneda lemma. In general, the other half– right to left– doesn’t automatically hold in an equipment.

In an equipment, the conjoint is the left adjoint of the companion. In the case of the Yoneda arrow, the adjunction reads:

$y^* \dashv y_*$

where $y^* = \hat A (1, y)$ . The adjunction can be illustrated using the following 2-cells:

with $K$ and $L$ arbitrary horizontal 1-cells.

The unit of this adjunction is generated by replacing $K$ with the unit and $L$ with $y_*$ .

Thus the unit provides us with the one-way mapping:

$1 \to y_* \odot y^*$

or, in expanded notation:

$A(1, 1) \to \hat A (y, 1) \odot \hat A (1, y)$

In a proarrow equipment, we can straighten the two arrows to get the 2-cell:

This is interpreted as a mapping from the unit arrow (horizontal-, thus elided) in $A$ , to the unit arrow in $\hat A$ . In $\mathbb{P}rof$ , this is a natural transformation from the hom-set in $A$ to the hom-set in the presheaf category. We recognize it as the action of the Yoneda functor on hom-sets. In fact in $\mathbb{P}rof$ it is an isomorphism:

$A(a, a') \cong \hat A (y a, y a') = [A, \mathbf{Set}](A(-, a), A(-, a'))$

which is the usual proof that the Yoneda embedding is fully faithful.

This is not an isomorphism in an arbitrary equipment, though.

We will therefore impose the condition that the unit of the adjunction $y^* \dashv y_*$ be an isomorphism. This, together with the density of $y$ will single out the equipments with the Yoneda structure. Such equipments have the presheaf objects and well-behaved Yoneda embeddings.

I’m grateful to John Baez for constructive criticism.

Appendix 1

The currying condition tells us that for any 0-cell $A$ there exist a pair $(\hat A, E \colon A \to \hat A)$ such that for any horizontal 1-cell $H \colon A \to B$ there exist a vertical 1-cell $f_H \colon B \to \hat A$ and the 2-cell $\xi$ :

In genereal, this doesn’t nail things down enough. There may be many candidates for $(\hat A, E \colon A \to \hat A)$ and many $f_H$ ‘s for a given $H$ .

What we want is to be able to reconstruct $H$ from $f_H$ . In other words we want currying to be an isomorphism, as it is in $\mathbb{P}rof$ :

$H \langle a b \rangle \cong E \langle a, f_H b \rangle$

This can be accomplished by requiring that the above 2-cell be a cartesian square. A cartesian square is defined by a universal condition with a trio of probes $(L, h, k)$ :

This might seem like a lot to process, but there is a trick to it. In $\mathbb{P}rof$ , we can replace $X$ and $Y$ with the terminal one-object/one-arrow category $1$ . A functor from such a category selects an object in the target category. Here, we pick two functors that select $a \colon A$ and $b \colon B$ :

The left hand side is a mapping $* \to E \langle a, f b \rangle$ . The right hand side is a horizontal composition of $* \to H \langle a, b \rangle$ and $H \langle a, b \rangle \to E \langle a, f b \rangle$ . The first one lets us fully reconstruct $H$ .

In a general double category we might not have a terminal 0-cell to select global elements, so we use the next best thing: generalized elements given by the trio $(L, h, k)$ .

July 19, 2026

Profunctor Optics

Posted by Bartosz Milewski under Category Theory, Haskell, Lens | Tags: Category Theory, Haskell, Lens, Optics, Profunctors, Tambara Modules |
Leave a Comment

You may think of Tannakian Reconstruction as an example of redundant encoding. It lets you replace a simple hom-set with a much more complex end that is taken over an entire functor category.

$C(a, b) \cong \int_{\hat F} Set (\hat F a, \hat F b)$

Why would anyone want to do it? The answer is simple: composition! Morphisms on the left compose according to the rules of the category $C$ , which can be arbitrarily complex. By contrast, the right hand side lives in $Set$ , and its elements are functions with very simple composition rules. So any time you want to internalize a non-trivial category in a programming language like Haskell, the Tannakian representation becomes a valuable tool. One such example is the category of optics.

Optics

A simple category of optics over a single category $C$ has objects that are pairs of objects $(a, b)$ . The morphisms are defined using the action of a monoidal category $\mathbf M$ (thus making $C$ an actegory):

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

In what follows, we’ll be using the fact that an element of a coend can be constructed by injecting a triple $(m, l, r)$ of an object $m : \mathbf M$ and a pair of morphisms:

$l \colon s \to m \triangleright a$
$r \colon m \triangleright b \to t$

Optics compose by “zooming in”:

$(s, t) \xrightarrow{O (s, t) (a, b)} (a, b) \xrightarrow{O (a, b) (a', b')} (a', b')$

The identity optic is given by injecting the triple $(1, \lambda_a^{-1}, \lambda_b)$ into the coend:

$O(a, b) (a, b) \in \int^{m \colon \mathbf M} C(a, m \triangleright a) \times C(m \triangleright b, b)$

where:

$\lambda_a \colon 1 \triangleright a \to a$

is the left unitor for the monoidal action and $1$ the unit object.

The archetypical optic is a lens, whose action is defined as the cartesian product in $C$ :

$L(s, t) (a, b) = \int^{m \colon C} C(s, m \times a) \times C(m \times b, t)$

In Haskell, we would encode it as an existential type:

			
data Lens s t a b = forall m .
    Lens (s -> (m, a)) ((m, b) -> t)

This formula can be expanded using the mapping-in property of the product (or, in an alternative derivation, its mapping out property, that is currying):

$\int^{m \colon C} C(s, m) \times C(s, a) \times C(m \times b, t)$

Using the Yoneda reduction (a.k.a. “integrating” over $m$ ), we get:

$C(s, a) \times C(s \times b, t)$

which, in Haskell, corresponds to a pair of functions:

			
get :: s -> a
set :: s -> b -> t

The getter extracts the subobject a, the focus of the lens. The setter replaces it with b.

Lenses compose by zooming in: the focus of one lens becomes the source of the other.

$(s, t) \xrightarrow{L (s, t) (a, b)} (a, b) \xrightarrow{L (a, b) (a', b')} (a', b')$

In Haskell this can be encoded as:

			
composeLens :: Lens a b a' b' -> Lens s t a b -> Lens s t a' b'
composeLens (Lens l2 r2) (Lens l1 r1) = Lens l3 r3
  where l3 = assoc' . second l2 . l1
        r3 = r1 . second r2 . assoc
        assoc ((c, c'), b')  = (c, (c', b'))
        assoc' (c, (c', a')) = ((c, c'), a')
  

		

As you can see, optic composition can be quite messy. That’s where the Tannakian representation saves the day.

Optics and Tambara modules

The idea is to follow the Tannakian reconstruction by defining the category of set-valued functors over the category of optics and use the end over these functors to represent optics.

It turns out that set-valued functors on optics are our old friends, Tambara modules. There is an equivalence of categories:

$[\mathbf{Opt}^{op}, Set] \cong \mathbf{Tamb}$

We use the opposite category of optics because, traditionally, optic composition is defiened in terms of zooming in rather than zooming out. Thus the slogan is: Presheaves on optics are Tambara modules.

Let’s first analyze the definition of a presheaf $\hat F \in [\mathbf{Opt}^{op}, Set]$ . On objects, it maps pairs $(a, b)$ to sets $\hat F (a, b)$ .

On morphisms, it maps optics to functions (reversing the direction). Thus an optic:

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

is mapped to a function:

$\hat F (O (s, t)(a, b)) \colon \hat F (a, b) \to \hat F (s, t)$ .

The plan is to construct two mappings: from presheaves to Tambara modules and another from Tambara modules to presheaves. They have to be defined on (pairs of) objects as well as on morphisms. I will first sketch the proof using category theory and then translate it, step by step, to Haskell.

From presheaf to Tambara

On objects, given a presheaf $\hat F$ , we define a profunctor:

$P a b = \hat F (a, b)$

We know that it’s a profunctor because, given a pair of morphisms:

$h \colon a' \to a$
$h' \colon b \to b'$

we can construct a mapping:

$\hat F(a, b) \to \hat F (a', b')$

We do this by lifting an optic of the type:

$\int^m C(a', m \triangleright a) \times C(m \triangleright b, b')$

This optic can be instantiated by injecting $(1, \lambda^{-1}_a \circ h, h' \circ \lambda_b)$ into the coend.

The tricky part is to equip $P$ with the Tambara structure:

$\lambda_{ m, a b} \colon P a b \to P (m \triangleright a)( m \triangleright b)$

In this case, we want to implement:

$\lambda_{ m, a b} \colon \hat F (a, b) \to \hat F (m \triangleright a, m \triangleright b)$

We’ll do this by lifting a carefuly chosen optic of the type:

$O (m \triangleright a, a) (m \triangleright b, b)$

This optic is given by the following coend:

$\int^n C(m \triangleright a, n \triangleright a) \times C(n \triangleright b, m \triangleright b)$

We instantiate it by injecting the triple $(m, id_{m \triangleright a}, id_{m \triangleright b})$ into the coend.

On morphisms, we want to map an optic to an element of the hom-set $Set (P a b, P s t)$ . This mapping itself is an element of a bigger hom-set:

$Set \big( \int^m C(s, m \triangleright a) \times C(m \triangleright b, t), Set (P a b, P s t) \big)$

Using the co-continuity of the hom-set, we replace the mapping out of a coend with the end:

$\int_m Set \big( C(s, m \triangleright a) \times C(m \triangleright b, t), Set (P a b, P s t) \big)$

We have at our disposal a pair of morphisms:

$l \colon s \to m \triangleright a$
$r \colon m \triangleright b \to t$

which, together with the Tambara structure, give us the desired mapping:

$P a b \xrightarrow{\lambda m, a b} P (m \triangleright a)( m \triangleright b) \xrightarrow{P\, l\, r} P s t$

From Tambara to presheaf

On objects, given a Tambara module $P$ , we define a presheaf :

$\hat F a b = P a b$

On morphisms, we have to map a function on Tambara modules $P a b \to P s t$ to an optic. To do that, we need to come up with a specific Tambara module to feed it to this function. Since we want to produce an optic, it makes sense that we feed it an optic. The question is: Are optics Tambara modules?

An optic $O (s, t) (a, b)$ is a profunctor in each pair of arguments. Let’s see if we can come up with a Tambara structure in $(s, t)$ while keeping the pair $(a, b)$ constant. Given:

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

We want to produce:

$\int^{m'} (C(m \triangleright s, m' \triangleright a) \times C(m' \triangleright b, m \triangleright t)$ .

We have at our disposal a pair of morphisms:

$l \colon s \to m' \triangleright a$
$r \colon m' \triangleright b \to t$

We know that simple hom-sets are Tambara modules, so we can apply the Tambara structure to both morphism:

$\lambda_{m, s, m' \triangleright a} \, l \colon m \triangleright s \to m \triangleright m' \triangleright a$
$\lambda_{m, m' \triangleright b} \, r \colon m \triangleright m' \triangleright b \to m \triangleright t$

After re-associating the iterated actions we inject the triple that consist of $m \otimes m'$ and the two resulting morphisms into our target coend.

Profunctor representation of optics

Since presheaves on $\mathbf{Opt}$ are Tambara modules, we can use the Tannakian reconstruction to represent a hom set in $\mathbf{Opt}$ as an end over Tambara modules:

$\int^{m \colon \mathbf M} C(s, m \triangleright a) \times C(m \triangleright b, t) \cong \int_{P \colon \mathbf{Tamb}} Set (P a b, P s t)$

This is the general form of the profunctor representation of optics that works for any monoidal action.

Haskell implementation

In Haskell, we can encode general optics (morphisms in $\mathbf{Opt}$ ) as:

			
data Opt ten act1 act2 s t a b = 
  forall m. (Actegory ten act1, Actegory ten act2) 
    => Opt (s -> m `act1` a) (m `act2` b -> t)

Notice that it’s okay to use two different actions (in fact, one can use two different categories). The corresponding Tambara modules are defined as:

			
class (Actegory ten act1, Actegory ten act2, Profunctor p) 
  => Tambara ten act1 act2 p where
    leftAct :: p a b -> p (m `act1` a) (m `act2` b)

The profunctor representation of these optics is given by a polymorphic function type:

			
type TamRep ten act1 act2 s t a b = 
    forall p . (Tambara ten act1 act2 p) => p a b -> p s t

Such functions can be composed (optics, zoomed in) using simple function composition.

Proof of equivalence

To prove the equivalence of the two representation, we need some additional definitions.

Here’s the unit optic that uses the unitors:

			
unitOpt :: (Actegory ten act1, Actegory ten act2) 
  => Opt ten act1 act2 a b a b
unitOpt = Opt unit' unit

Since we are working with the oposite category, we define the flipped version of optics:

			
data FlipOpt ten act1 act2 a b s t 
   = FlipOpt (Opt ten act1 act2 s t a b)

FlipOpt is an instance of Tambara:

			
instance (Actegory ten act1, Actegory ten act2) 
  => Tambara ten act1 act2 (FlipOpt ten act1 act2 a b) where
    leftAct (FlipOpt (Opt l r)) = FlipOpt (Opt l' r') 
      -- take advantage of the Tambara structure on hom-sets
      -- l :: s -> m a, l' :: n s -> n m a
      -- r :: m b -> t, r' :: n m b -> n t
      where l' = assoc' . leftAct @ten @act1 @act1 @(->) l
            r' =          leftAct @ten @act2 @act2 @(->) r . assoc
  

		

I made the use of the Tambara action on hom-functors explicit through type annotations.

Here’s the mapping from optics to the Tambara representation:

			
toProRep :: (Actegory ten act1, Actegory ten act2) => 
  Opt ten act1 act2 s t a b -> TamRep ten act1 act2 s t a b
toProRep (Opt s_ma mb_t) pab = dimap s_ma mb_t (leftAct pab)

The opposite mapping uses the flipped unit optics. This is why we needed the proof that flipped optic is a Tambara module. As such, we can pass it to our function that is polymorphic in Tambara modules:

			
fromProRep ::  (Actegory ten act1, Actegory ten act2) => 
  TamRep ten act1 act2 s t a b -> Opt ten act1 act2 s t a b
fromProRep pab_pst = opt
  where FlipOpt opt = pab_pst (FlipOpt unitOpt)

Examples

By plugging in different monoidal categories and their actions, we can immediately generate Tambara representations for a variety of optics.

We can use the Tambara encoding for the lens:

			
type Lens s t a b = forall p . 
  Tambara (,) (,) (,) p => p a b -> p s t

Here’s the example of a prism:

			
data Prism s t a b = forall m .
    Prism (s -> Either m a) (Either m b -> t)

and its Tambara representation:

			
type Prism' s t a b = forall p . 
  Tambara Either Either Either p => p a b -> p s t

Haskell code for this post is available here.

July 14, 2026

Tannakian reconstruction

Posted by Bartosz Milewski under Category Theory | Tags: Category Theory, Fiber Functor, Tannakian Reconstruction |
1 Comment

Two friends, Alice and Bob, live in the same city, but on the opposite sides of a wide river. Every night, Bob looks at the lights on the other side and tries to guess, which one belongs to Alice. They come up with a clever arrangement: Alice will turn on her lights for 10 minutes every night at 10 p.m. Every night Bob will take a long-exposure photo at the pre-arranged time. At the end of the year, Bob will superimpose all the photos, and hopefully the only bright spot will be Alice’s window. This is Tannakian reconstruction in a nutshell.

A functor produces a picture of one category inside another. It’s a potentially lossy encoding, but it always preserves the structure of the source. If there is a connection (morphism) between two objects in the source category, there will always be a connection between their images in the target category.

In general it’s impossible to recover the structure of the source category by looking at only one such picture. But if the target category has enough resolution, and we superimpose all available pictures, we can recover the morphisms of the source category.

Fiber functors

A category with just the right resolution is the category of sets. Therefore we’ll be looking at functors in $[C, Set]$ (for historical reasons, these are called co-presheaves). Such a functor maps objects to sets, and morphisms to functions.

When dealing with functors, we usually imagine varying objects and morphisms while keeping the functor constant. Here, we are interested in using the totality of all functors while keeping the objects constant. To every object $c \colon C$ we will associate a mapping from functors to sets, simply by applying each functor to this object $c$ :

$\Phi_c \colon [C, Set] \to Set$

$\Phi_c \hat F = \hat F c$

This mapping is functorial. Indeed, a natural transformation between $\hat F$ and $\hat G$ is a family of functions $\alpha_a \colon \hat F a \to \hat G a$ . We define the action of $\Phi_c$ on a natural transformation by taking its component $\alpha_c$ .

$\Phi_a$ is called a fiber functor. You may think of it as probing an object and, through morphisms, its immediate neighborhood.

Tannakian reconstruction

To probe a hom-set $C(a, b)$ we’ll be looking at the set of functions $\hat F a \to \hat F b$ under all possible functors $\hat F \colon C \to Set$ .

This set happens to be the set of natural transformations between two fiber functors $\Phi_a$ and $\Phi_b$ , a hom-set in the functor category:

$[[C, Set], Set] (\Phi_a, \Phi_b)$

A set of natural transformations can be written as an end:

$\int_{\hat F \colon [C, Set]} Set (\Phi_a \hat F, \Phi_b \hat F) = \int_{\hat F \colon [C, Set]} Set (\hat F a, \hat F b)$

An end is like a gigantic product. In our analogy, it correspond to the superposition of all photos. Like with any product, if any of its components is empty, the whole end is empty. Since the end goes over every possible functor, what prevents us from hand-picking a functor that’s non-empty at $a$ and empty at $b$ ? Such a single bad apple would spoil the whole batch (there is no function from a non-empty set to an empty set).

What makes this end non-trivial is functoriality. Any time there is a morphism $f \colon a \to b$ , we automatically have a function $\hat F a \to \hat F b$ , for any functor $\hat F$ . In fact, because of the Yoneda embedding being full and faithful, we have as many such functions as there are morphisms in $C(a, b)$ . We have the isomorphism:

$\int_{\hat F} Set (\hat F a, \hat F b) \cong C(a, b)$

By superimposing the images of all functors, we recover the original hom-set. This is the categorical version of Tannakian reconstruction.

We’ll use the double-Yoneda trick to prove it. First, we use the Yoneda lemma:

$[C, Set] (C(a, -), \hat F) \cong \hat F a$

to explode the functors under the end:

$\int_{\hat F} Set ([C, Set] (C(a,-), \hat F), [C, Set] (C(b, -), \hat F)$

We can now apply the Yoneda reduction to “integrate” over $\hat F$ . The result is:

$[C, Set] (C(b, -), C(a, -))$

which, again by Yoneda, is equivalent to:

$C(a, b)$

As an example, let’s apply Tannakian reconstruction to a simple one-object category. Such a category has a single hom set, which forms a monoid under composition. A set-valued functor maps the single object of $C$ to a set — a representation of this monoid. Natural transformations between such functors are called equivariant maps. Tannakian reconstruction lets us recover the monoid from the totality of its representations. Notice that naturality/equivariance is baked into the definition of an end.

July 11, 2026

Tambara Equipment

Posted by Bartosz Milewski under Category Theory, Double category | Tags: Category Theory, Double Categories, Optics, Proarrow Equipment, Profunctors, Tambara Modules |
[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.

June 30, 2026

Actegories

Posted by Bartosz Milewski under Category Theory, Haskell | Tags: Actegories, Category Theory, Haskell, Lens, Optics |
Leave a Comment

Previously: Kan Extensions in Double Categories.

In programming, actegories play a central role in optics: lenses, prisms, traversals, etc. To understand actegories, let’s start with the definition of a monoidal category.

Monoidal Category

A monoidal category $\mathbf M$ is a category equipped with a tensor product. A tensor product is a functor $\otimes \colon \mathbf M \times \mathbf M \to \mathbf M$ . We assume that this product is associative and unital– up to isomorphism. It means that there is an invertible associator:

$\alpha_{a, b, c} \colon (a \otimes b) \otimes c \to a \otimes (b \otimes c)$

natural in all three arguments. We also have a unit object $1$ and two (invertible, natural) unitors:

$\lambda_a \colon 1 \otimes a \to a$

$\rho_a \colon a \otimes 1 \to a$

To get a better feel for it, we can try to model a monoidal category in Haskell. We parameterize it by the type of the tensor product, ten, which we want to be a Bifunctor:

class (Bifunctor ten) => MonoidalCategory ten where ...

The standard way to define a subcategory of Hask is to restrict the types of objects by imposing a constraint. Such a restriction has a special kind, Constraint:

			
class Bifunctor ten
  => MonoidalCategory (obj :: Type -> Constraint) ten where ...

A common example of such a constraint is a typeclass. For instance Monoid will restrict the objects of the category to be monoids. (In principle, we should also restrict the type of arrows, here to monoid morphisms.)

We can specify the unit of a monoidal category as an associated type (parameterized by ten):

    type Unit ten :: Type

The unit should be an object of the category, so it should satisfy the constraint. We can encode this in our definition as a precondition: obj (Unit ten). This leads to a circularity, which we can overcome using the language pragma UndecidableSuperClasses:

			
class (Bifunctor ten , obj (Unit ten))
  => MonoidalCategory (obj :: Type -> Constraint) ten where
    type Unit ten :: Type
    ...

Finally, we can add the associator and the unitors (and their inverses):

			
class (Bifunctor ten , obj (Unit ten))
  => MonoidalCategory (obj :: Type -> Constraint) ten where
    type Unit ten :: Type
    alpha  :: (obj a, obj b, obj c) =>  (a `ten` b) `ten` c -> a `ten` (b `ten` c)
    lambda :: (obj a) => (Unit ten) `ten` a -> a
    ...

		

Notice the obj constraints in the type of these functions and the infix notation for the tensor.

Let’s work out a few examples. The simplest is the category of all types with a cartesian product as tensor.

			
instance MonoidalCategory Hask (,) where
    type Unit (,) = ()
    alpha ((a, b), c) = (a, (b, c))
    lambda ((), a) = a
    ...

		

We define Hask using an empty class, and we make all objects its instances:

			
class Hask a
instance Hask a

Similarly, we can define a monoidal category with Either as the tensor product, or with Monoid as the object constraint.

Actegory

An actegory is a category that supports the action of a monoidal category. You may think of it as “multiplying” or “scaling” the objects of this category by objects of the monoidal category. The (left) action can be defined as a functor from the product category to $C$ :

$\triangleright \colon \mathbf M \times C \to C$

or, after currying, as a functor from $\mathbf M$ to the endofunctor category:

$\triangleright \colon \mathbf M \to [C, C]$

The coherency conditions are the invertible natural transformations that relate the action $\triangleright$ to the tensor product $\otimes$ and its unit $1$ :

$\alpha_{m n a} \colon (m \otimes n) \triangleright a \to m \triangleright (n \triangleright a)$

$\lambda_{a} \colon 1 \triangleright a \to a$

The action is functorial in both arguments, so our Haskell translation pegs it, for simplicity, as a Bifunctor. (A Profunctor action is also possible. Categorically, it would correspond to using $\mathbf M^{op}$ as the monoidal category.)

			
class (MonoidalCategory obj ten, Bifunctor act) 
  => Actegory obj ten act | act -> ten where
    assoc  :: (obj m, obj n) 
           => (m `ten` n) `act` a -> m `act` (n `act` a)
    assoc' :: (obj m, obj n)
           => m `act` (n `act` a) -> (m `ten` n) `act` a
    unit   :: Unit ten `act` a -> a
    unit'  :: a -> Unit ten `act` a

		

Another simplifying assumption is that the action uniquely identifies the tensor product, encoded here as the functional dependency act -> ten.

The simplest example of an actegory is the self action of the cartesian product. Here, the monoidal category acts on itself:

			
instance Actegory Hask (,) (,) where
    assoc ((m, n), a) = (m, (n, a))
    assoc' (m, (n, a)) = ((m, n), a)
    unit ((), a) = a
    unit' a = ((), a)

		

Monoidal Functors

Actegories that use the same monoidal category for their actions form a category. The morphisms in this category are (strict) monoidal functors. These are functors that map one action to another:

$f (m \triangleright_1 a) \cong m \triangleright _2 f a$

In Haskell, we can model them as:

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

In fact, actegories form a bicategory, with action-preserving natural transformations acting between monoidal functors.

Here’s an interesting example of a monoidal functor between non-trivial actegories:

			
instance (Traversable f) => MonFunctor Monoid (,) (,) (,) f where
    as (m, fa) = fmap (m, ) fa
    as' = sequenceA

Haskell code is available here.

June 13, 2026

Kan Extensions in Double Categories

Posted by Bartosz Milewski under Category Theory, Double category, Haskell, Kan extensions, Profunctor Equipment | Tags: Category Theory, Double Category, Profunctors |
Leave a Comment

Previously: Kan extensions in Haskell.

In a double category that is also a proarrow equipment, we have the ability to bend arrows. In particular, in the definition of the counit of the right Kan extension:

we can bend the vertical $j$ arrow, replacing it with its horizontal conjoint $B(1, j)$ . In a profunctor equipment, this is just a representable profunctor $\langle b, a\rangle \mapsto B(b, j a)$ .

A natural generalization is to replace this representable with a general profunctor. This way we get a definition of a right Kan extension along a profunctor $J$ .

In a more general setting of a double category, the counit of the right Kan extension is a 2-cell:

The universal condition can be similarly generalized by bending the $j$ arrows.

However, the universal condition for pointwise right Kan extensions is stronger. It involves an additional horizontal 1-cell $H$ . It states that any 2-cell $\phi$ of the shape below can be uniquely factorized through the counit $\epsilon$ :

Right Kan extensions in Haskell

In Haskell, the right Kan extension of a functor d along a profunctor j can be written as a data type:

newtype Ran j d a = Ran (forall x . j a x -> d x)

This is a direct translation of the categorical formula that uses an end:

$(\text{Ran}_J d) \, a = \int_x \text{Set}(J a x, d \, x)$

Compare this with the earlier implementation of the Kan extension, in which j was a functor:

newtype Ran j d a = Ran (forall x . (a -> j x) -> d x)

The counit is a 2-cell from j to the identity profunctor (->):

			
epsilon :: (Profunctor j, Functor d) => 
  Cell (Ran j d) d j (->)
epsilon jab (Ran ran) = ran jab

The 2-cell Phi goes from the profunctor composition of j and h to the identity profunctor:

type Phi s d j h  = Cell s d (Procompose j h) (->)

The factorization cell Phi' goes from h to identity:

type Phi' s d j h = Cell s (Ran j d) h (->)

For any Phi, we can find the corresponding Phi':

			
rightAdj :: (Profunctor j, Profunctor h, Functor d, Functor s) =>
        Phi s d j h -> Phi' s d j h
rightAdj phi hac sa = Ran (\ jcb -> phi (Procompose jcb hac) sa)

This function replaces the right adjoint used in the traditional definition of a Kan extension.

The result satisfies the factorization property:

			
factor :: (Profunctor j, Profunctor h, Functor d, Functor s) => 
  Phi s d j h -> Phi s d j h
factor phi = funComp . vcomp (rightAdj phi) epsilon

Here vcomp is the vertical composition of 2-cells:

			
vcomp :: (Functor f, Functor g, Functor h
         , Profunctor p, Profunctor q, Profunctor r, Profunctor s) =>
  Cell f g p r -> Cell g h q s 
  -> Cell f h (Procompose q p) (Procompose s r)
vcomp fg_pr gh_qs (Procompose qxc pax) 
    = Procompose (gh_qs qxc) (fg_pr pax)

		

and funComp is hom-functor composition:

			
funComp :: Procompose (->) (->) a b -> (a -> b)
funComp (Procompose f g) = f . g

The computational meaning of the universal construction is that, in order to define a 2-cell (natural transformation) from some functor s to Ran j d along a profunctor h, it’s enough to provide a 2-cell from s to d along a composite Procompose j h.

Left Kan extensions

We can apply similar generalization to left Kan extensions. This time we start with the unit given by the 2-cell:

The universal condition that defines the pointwise left Kan extension of a vertical 1-cell $d$ along a horizontal 1-cell $J$ is given by the following unique factorization:

Left Kan extensions in Haskell

In Haskell, we define the left Kan extension along a profunctor as an existential data type:

			
data Lan j d a where
    Lan :: j x a -> d x -> Lan j d a

This is a direct translation of the coend formula:

$(\text{Lan}_J d)\, a = \int^x ( J x a \times d \,x)$

The unit is a 2-cell:

			
eta :: (Profunctor j, Functor d) => Cell d (Lan j d) j (->)
eta jab da = Lan jab da

The universal condition states that, for any 2-cell:

type Phi s d j h  = Cell d s (Procompose h j) (->)

there is a unique 2-cell:

type Phi' s d j h = Cell (Lan j d) s h (->)

given by the mapping:

			
leftAdj :: (Profunctor j, Profunctor h, Functor d, Functor s) =>
        Phi s d j h -> Phi' s d j h
leftAdj phi hac (Lan jxa dx) = phi (Procompose hac jxa) dx

that uniquely factorizes through the unit eta:

			
factor :: (Profunctor j, Profunctor h, Functor d, Functor s) =>
    Phi s d j h -> Phi s d j h
factor phi = funComp . vcomp eta (leftAdj phi)

Again, computationally, this defines a mapping-out property of the left Kan extension.

Complete Haskell code is available here: left Kan extensions, right Kan extensions.

June 8, 2026

Kan Extensions in Haskell

Posted by Bartosz Milewski under Category Theory, Haskell, Programming | Tags: Category Theory, Haskell, Kan extensions, Universal Arrows |
1 Comment

Previously: Tabulation Tribulations.

If you think of functor composition as a form of multiplication, Kan extensions are an attempt to construct inverses of this multiplication. But unlike multiplication, composition is not symmetric, so we have extensions that attempt to undo precomposition, and lifts that do the same for postcomposition. Furthermore, there rarely is a single inverse to any form of composition, so we have the parsimonious right extensions and lifts, and the generous left extensions and lifts. We end up with four combinations that correspond to four different adjunctions:

$(- \circ j) \dashv \text{Ran}_j -$

$\text{Lan}_j - \dashv (- \circ j )$

$(j \circ -) \dashv \text{Rift}_j -$

$\text{Lift}_j - \dashv (j \circ -)$

We’ll concentrate on the extensions, since we can provide explicit point-wise formulas for them in cases that are of interest to us, that is in $\mathbf{Cat}$ and in $\mathbb{P}rof$ .

Right Kan extensions

The definition of the right Kan extension relates the mapping out of the composition to the mapping into $\text{Ran}$ . In Haskell, we can define them as two types:

			
type Phi  j s d = Compose s j ~> d
type Phi' j s d = s ~> Ran j d

The wavy arrows denote natural transformations:

type f ~> g = forall x. f x -> g x

To show that there is an adjunction we can either prove the (natural) isomorphism between Phi and Phi', or implement the unit and counit of the adjunction (together with zigzag identities):

			
eta     :: (Functor j, Functor d) => d ~> Ran j (Compose d j)
epsilon :: (Functor j, Functor d) => Compose (Ran j d) j ~> d

In Haskell we can implement the right Kan extension as:

newtype Ran j d a = Ran (forall x . (a -> j x) -> d x)

This is a straightforward translation of the categorical formula that uses an end:

$(\text{Ran}_j d) \,a = \int_x \text{Set}(C(a, j \,x), d \, x)$

The adjunction can then be implemented as a pair of mappings:

			
leftAdj :: (Functor j, Functor d, Functor s) =>
   Phi j s d -> Phi' j s d
leftAdj phi sx = Ran (\x_jx -> phi (Compose (fmap x_jx sx)))
rightAdj ::  (Functor j, Functor d, Functor s) =>
   Phi' j s d -> Phi j s d
rightAdj phi' (Compose sj) = 
    let (Ran ran) = phi' sj
    in ran id

		

Or as the unit/counit pair:

			
eta :: (Functor j, Functor d) => d ~> Ran j (Compose d j)
eta dx = Ran (\x_jx -> Compose (fmap x_jx dx))
epsilon :: (Functor j, Functor d) => Compose (Ran j d) j ~> d
epsilon (Compose (Ran ran)) = ran id

Universal arrows

There is a third way, which gives a better starting point for generalizations. It can be used on an object-by-object basis, even if there is no global adjunction. It’s based on the idea of the universal arrow.

A universal arrow is a terminal object in the comma category. For a given functor $L \colon D \to C$ , the comma category $L/c$ consists of pairs $(d, f \colon L d \to c)$ . In other words, it’s a category of arrows from the image of $L$ to some fixed object $c \in C$ . Morphisms in the comma category are arrows $h: d \to d'$ in $D$ that make the corresponding triangles in $C$ commute:

A terminal object in $L/c$ is a pair $(t, \tau)$ , through which every arrow $\Phi \colon L d \to c$ factorizes uniquely. That means, there is a unique arrow $h \colon d \to t$ that makes the following triangle commute:

If there is an adjunction $L \dashv R$ , then we can easily construct the universal arrow as a pair $(R c, \epsilon_c)$ , where $\epsilon_c$ is a component of the counit of the adjunction. Indeed, every $\Phi \colon L d \to c$ factorizes through $\epsilon_c$ :

$\Phi = \epsilon_c \circ L \Phi'$

where $\Phi' = \text{leftAdj}\, \Phi$ .

The advantage of the universal arrow approach is that it’s pointwise. We can do it for each object $c$ separately.

Reversing this process, rather than building an adjuncion, we can directly construct a universal arrow. We start by defining of a component of a counit. Then we postulate that any other counit-like mapping factorizes uniquely throught that counit.

Let’s see how it works for our definition of the right Kan extension. The counit has the following signature:

epsilon :: (Functor j, Functor d) => Compose (Ran j d) j ~> d

We can illustrate it with the following string diagram:

In general, the functors go between three different categories: A, B, and M. In Haskell we have just one category and three endofunctors.

Any other mapping of this form has the signature (replacing Ran j d with an arbitrary functor s):

type Phi j s d = Compose s j ~> d

Or, as a string diagram:

We postulate that, for every Phi, there is a unique Phi' that factorizes it through epsilon. That is, we have a function:

			
leftAdj :: (Functor j, Functor d, Functor s) =>
   Phi j s d -> Phi' j s d

such that:

			
factor :: (Functor j, Functor d, Functor s) => Phi j s d -> Phi j s d
factor phi = epsilon . Compose . leftAdj phi . getCompose

Modulo newtype shenanigans, this is exactly $\epsilon \circ (L_j \Phi')$ , where $L_j s = s \circ j$ is functor precomposition. Or as a string diagram:

Notice that rightAdj doesn’t appear anywhere in this construction.

The computational interpretation of this universal construction lets us calculate a mapping into a right Kan extension. Namely, to determine a natural transformation from some functor s to Ran j d, it’s enough to provide a mapping phi from Compose s j to d.

Left Kan extensions

We can now apply the same idea to the left Kan extension. This time we start with the unit:

eta :: (Functor j, Functor d) => d ~> Compose (Lan j d) j

We postulate that for any other mapping of this form (replacing Lan j d with and arbitrary s):

type Phi j s d = d ~> Compose s j

there is a unique Phi':

type Phi' j s d = Lan j d ~> s

that factorizes it through eta:

			
factor :: (Functor j, Functor d, Functor s) => Phi j s d -> Phi j s d
factor phi = Compose . rightAdj phi . getCompose . eta

In Haskell, the left Kan extension is given by the existential data type:

			
data Lan j d a where
    Lan :: (j x -> a) -> d x -> Lan j d a

In category theory, this formula uses a coend:

$(\text{Lan}_j d) \, a = \int^x C(j \, x, a) \times d \, x$

Indeed, for any given Phi, we can obtain a Phi' by applying this function:

			
rightAdj :: (Functor j, Functor d, Functor s) =>
   Phi j s d -> Phi' j s d
rightAdj d_sj (Lan jx_a dx) = 
    let Compose sjx = d_sj dx
    in fmap jx_a sjx

		

The result factorizes Phi through eta:

			
factor :: (Functor j, Functor d, Functor s) => Phi j s d -> Phi j s d
factor phi = Compose . rightAdj phi . getCompose . eta

The computational interpretation of this universal construction let us calculate a mapping out of the left Kan extension.

See Haskell code for right and left Kan extensions.

Next, we’ll generalize these construction to a double category setting.

May 23, 2026

Tabulation Tribulations

Posted by Bartosz Milewski under Category Theory | Tags: Category Theory, Double Categories, Profunctor Equipment, Profunctors |
Leave a Comment

Previously: Bending, Yanking, and Cartesian Squares in Double Categories.

We all know what a graph of a function is: it’s a set of pairs $(a, b)$ , where $b = f a$ . Similarly, a graph of a relation is a set of pairs where $b$ is related to $a$ .

A profunctor can be viewed as a proof-relevant relation. So a graph of a profunctor is a triple, which contains two objects and a proof, or a witness, that they are related. The witness in this case is any element of the set $J \langle a, b \rangle$ . If the set is empty, it means that the objects are unrelated.

Such triples form a category, which is often called the category of elements of a profunctor.

Given a profunctor $J \colon A^{op} \times B \to Set$ , an object in the category of elements is a triple $(a, j, b)$ . We interpret $j \in J \langle a, b \rangle$ as a witness that $a$ is related to $b$ .

A morphism in the category of elements between $(a, j, b)$ and $(a', j', b')$ is a pair of morphisms $(u \colon a \to a', v \colon b \to b')$ such that:

$J \langle a, v \rangle \,j = J \langle u, b' \rangle \, j'$

Here $J \langle a, v \rangle = J \langle id_a, v \rangle$ is the whiskering, or the lifting of a pair of morphisms, one of which is an identity, by the profunctor $J$ ; and similarly for $J \langle u, b' \rangle$ . We want the result, in both cases, to give us the same element of $J \langle a, b' \rangle$ — the witness that $a$ is related to $b'$ .

The analog of a graph of a profunctor in a double category is called a tabulation. A tabulation of a horizontal arrow $J \colon A \to B$ is a 0-cell $\langle J \rangle$ equipped with two projections. Think of these projections as extracting the two objects from the triple that we used in the definition of a graph of a profunctor. Their relation to $J$ is illustrated by the following 2-cell:

Let’s see how this works in $\mathbb{P}rof$ . Here we have a typical square that we’ve seen before, except that there is an invisible identity profunctor on the left — a hom-functor in the category $\langle J \rangle$ . The square tells us that for every morphism in $\langle J \rangle$ we can find a corresponding element of the profunctor $J$

Let’s pick two objects (triples) in $\langle J \rangle$ and a hom set between them:

$\langle J \rangle ((a, j, b), (a', j', b'))$

An element of this hom-set is a pair of morphisms $(u \colon a \to a', v \colon b \to b')$ . The 2-cell $\pi$ is a natural transformation whose components are:

$\pi_{(a, j, b)(a', j', b')} \colon \langle J \rangle ((a, j, b), (a', j', b')) \to J ( \pi_A (a, j, b), \pi_B (a', j', b'))$

Using our definitions, the argument of this mapping is a pair $(u, v)$ and the result is an element of the set $J(a, b')$ .

The mapping can be instantiated either by the lifting (whiskering) of $u$ or $v$ , both leading to the same result.

In a double category, we define a tabulation using its universal property. Just like a categorical product is universally defined by its mapping-in condition, so is a tabulation. However, since we are now working in a double category, besides the 1-dimensional mapping-in condition, we also need a 2-dimensional condition for 2-cells.

1-dimensional condition

What makes the projections projections is the mapping-in condition from some arbitrary 0-cell $X$ . We postulate that for any 0-cell $X$ that is equipped with two 1-cells $\phi_A$ and $\phi_B$ there is a unique factorization through the universal 2-cell $\pi$ :

In $\mathbb{P}rof$ , these 2-cells correspond to natural transformations:

$\phi_{x, x'} \colon X(x, x') \to J(\phi_A x, \phi_B x')$

$(\pi \circ id_{\phi'})_{x, x'} \colon X(x, x') \to J (\pi_A (\phi' x), \pi_B (\phi' x'))$

We can then define $\phi'$ , on objects, as:

$\phi' x = (\phi_A x, \phi_{x, x} id_x, \phi_B x)$

and acting on a morphism $f \colon x \to x'$ , as $(\phi_A f, \phi_B f)$ .

To summarize, the 1-dimensional condition lets us construct a vertical mapping $\phi' \colon X \to \langle J \rangle$ . All we have to provide is two vertical arrows and a 2-cell. But to complete the picture, we should be able to construct a 2-cell from another horizontal 1-cell, $H$ . For that we need a 2-dimensional universal condition.

2-dimensional condition

A 2-dimensional condition combines two instances of the one-dimensional condition. The second instance is another 0-cell $Y$ together with a projection $\psi$ , such that:

Using these two instances, we want to construct a mapping out of a horizontal 1-cell $H$ . There are two ways of combining these two instances on top of each other, and we postulate that the resulting 2-cells be equal:

In $\mathbb{P}rof$ , this corresponds to two natural transformations:

$\xi_{A\, x, y} \colon H(x, y) \to A(\phi_A x, \psi_A y)$
$\xi_{B\, x, y} \colon H(x, y) \to B(\phi_B x, \psi_B y)$

with the two composites equal:

$H(x, y) \to \int^{y'} A (\phi_A x, \psi_A y') \times J(\psi_A y', \psi_B y)$
$H(x, y) \to \int^{x'} J (\phi_A x, \phi_B x') \times B(\phi_B x', \psi_B y)$

The two-dimensional universal condition then statest that there is a unique 2-cell $\xi'$ :

such that both $\xi_A$ and $\xi_B$ factor through it. Here’s the first factorization:

In $\mathbb{P}rof$ , $\xi'$ is a natural transformation with a component:

$\xi'_{x, y} \colon H(x, y) \to \langle J \rangle (\phi' x, \psi' y)$

Substituting our definitions of $\phi'$ and $\psi'$ , we get as the target a pair of morphisms:

$(u \colon \phi_A x \to \psi_A y, v \colon \phi_B x \to \psi_B y)$

Given $h \in H (x, y)$ , we can construct such a pair as:

$( \xi_{A\, x, y} h, \xi_{B\, x, y} h)$

When followed by $id_{\pi_A}$ this produces $\xi_{A x, y}$ thus satisfying the 2-dimensional universal condition. The constraints on $\xi_A$ and $\xi_B$ ensure that the pair of morphisms is indeed a proper morphism in $\langle J \rangle$ .

The same argument works when we replace $A$ with $B$ .

From the practical point of view, the 2-dimensional condition lets us construct a mapping (a 2-cell) $\xi'$ from a horizontal 1-cell $H$ to $\langle J \rangle$ using a pair of mappings into $A$ and $B$ satisfying coherency conditions.

The advantage of the universal construction is that it avoids talking about individual sets or, for that matter, about the category of sets. It thus works out of the box for enriched profunctors and other exotic embodiments of double categories.

Twisted Arrow Category

Cocones

From Cocones to Cowedges

Twisted Optics

Right Kan Lift

Tannakian Reconstruction

Overview

Classifying Arrows

Yoneda Embedding

The Adjunction

Appendix 1

Optics

Optics and Tambara modules

From presheaf to Tambara

From Tambara to presheaf

Profunctor representation of optics

Haskell implementation

Proof of equivalence

Examples

Fiber functors

Tannakian reconstruction

Monoidal functors redux

Tambara modules

Tambara Equipment

Free Tambara and Optics

Internalizing monoidal actions

Internal monoid

Monoidal Category

Actegory

Monoidal Functors

Right Kan extensions in Haskell

Left Kan extensions

Left Kan extensions in Haskell

Right Kan extensions

Universal arrows

Left Kan extensions

1-dimensional condition

2-dimensional condition

Top Posts

License

Blogroll

Follow Me

Archives