June 13, 2026

Kan Extensions in Double Categories

Posted by Bartosz Milewski under Category Theory, Double category, Haskell, Kan extensions, Profunctor Equipment | Tags: , , |
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.

 

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.