Kan Extensions in Double Categories | Bartosz Milewski's Programming Cafe
Home
About
Bartosz Milewski's Programming Cafe
Category Theory, Haskell, Concurrency, C++
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 arrow, replacing it with its horizontal conjoint . In a profunctor equipment, this is just a representable profunctor .
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 .
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 arrows.
However, the universal condition for pointwise right Kan extensions is stronger. It involves an additional horizontal 1-cell . It states that any 2-cell of the shape below can be uniquely factorized through the counit :
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:
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) =><br>Cell (Ran j d) d j (->)<br>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) =><br>Phi s d j h -> Phi' s d j h<br>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) =><br>Phi s d j h -> Phi s d j h<br>factor phi = funComp . vcomp (rightAdj phi) epsilon
Here vcomp is the vertical composition of 2-cells:
vcomp :: (Functor f, Functor g, Functor h<br>, Profunctor p, Profunctor q, Profunctor r, Profunctor s) =><br>Cell f g p r -> Cell g h q s<br>-> Cell f h (Procompose q p) (Procompose s r)<br>vcomp fg_pr gh_qs (Procompose qxc pax)<br>= Procompose (gh_qs qxc) (fg_pr pax)
and funComp is hom-functor composition:
funComp :: Procompose (->) (->) a b -> (a -> b)<br>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 along a horizontal 1-cell 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<br>Lan :: j x a -> d x -> Lan j d a
This is a direct translation of the coend formula:
The unit is a 2-cell:
eta :: (Profunctor j, Functor d) => Cell d (Lan j d) j (->)<br>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) =><br>Phi s d j h -> Phi' s d j h<br>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) =><br>Phi s d j h -> Phi s d j h<br>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.
Share this:
Share on Reddit (Opens in new window)<br>Reddit
More
Share on X (Opens in new window)
Share on LinkedIn (Opens in new window)<br>LinkedIn
Share on Facebook (Opens in new window)<br>Facebook
Email a link to a friend (Opens in new window)<br>Email
Like this:<br>Like Loading…
Related
Leave a ReplyCancel...