Roughly speaking, the observation is that in the category of profunctors (over small sets), there is an idempotent monad \(\bigcirc \) for turning profunctors into functors (over small sets). Consequently, if we want to do some constructions for functors, we can work in the better behaved category of profunctors instead and use the modality \(\bigcirc \) to enter the world of functors when necessary.

In this post, we assume that we have two (cumulative) universes of sets \(\mathbf {Set}_s \in \mathbf {Set}_l\) (small sets and large sets). The profunctor category \([\mathbf {Set}_s^{\mathrm {op}} \times {\mathbf {Set}_s}, \mathbf {Set}_l]\) is denoted by \(\mathbf {P}\) and the functor category \([\mathbf {Set}_s, \mathbf {Set}_l]\) is denoted by \(\mathbf {F}\). Because \(\mathbf {Set}_s\) is smaller than \(\mathbf {Set}_l\), both \(\mathbf {F}\) and \(\mathbf {P}\) are presheaf categories \[ \mathbf {F} = \mathbf {Pr}(\mathbf {Set}_s^{\mathrm {op}}) \qquad \text { and }\qquad \mathbf {P} = \mathbf {Pr}(\mathbf {Set}_s \times \mathbf {Set}_s^{\mathrm {op}}), \] with nice properties and structures that we all love.

We need the universe \(\mathbf {Set}_l\) of large sets to be large enough for doing usual category theory (say, a Grothendieck universe), but the smaller universe \(\mathbf {Set}_s\) only needs to have the terminal set \(1\) and be closed under \(\Sigma \)-types. For example, we can choose \(\mathbf {Set}_s\) to be the set \(\mathbf {Fin}\) of (standard) finite sets. If you are programming in a language with an impredicative universe, you can use it for both \(\mathbf {Set}_s\) and \(\mathbf {Set}_l\).

Our starting point is the functor \(R : \mathbf {P} \to \mathbf {F}\) defined by \[ (RP)(b) = P(1, b) \] that constantly supplies the terminal set \(1\) to the contravariant position of the profunctor \(P\). This functor \(R : \mathbf {P} \to \mathbf {F}\) can be viewed as the change-of-base functor between the presheaf categories \(\mathbf {P}\) and \(\mathbf {F}\) along the functor \(\rho : \mathbf {Set}_s^{\mathrm {op}} \to \mathbf {Set}_s \times \mathbf {Set}_s^{\mathrm {op}}\): \[ \rho (b) = (1, b), \] so we know that \(R : \mathbf {P} \to \mathbf {F}\) has both a left adjoint and a right adjoint by Kan extension.

What are the two adjoints of \(R : \mathbf {P} \to \mathbf {F}\)? It turns out they are exactly the two natural ways to embed functors in profunctors:

• We can use a functor as a profunctor by its Kleisli embedding: the functor \(K : \mathbf {F} \to \mathbf {P}\) is defined by \[ (KF)(a, b) = (a \Rightarrow F b) \] where \(a \Rightarrow F b\) is the set of functions from \(a \in \mathbf {Set}_s\) to \(F b \in \mathbf {Set}_l\). The functor \(K\) is fully faithful.
• We can use a functor as a profunctor by ignoring the contravariant argument: the functor \(L : \mathbf {F} \to \mathbf {P}\) is defined by \[ (LF)(a,b) = F b. \] The functor \(L\) is also fully faithful.

Now we have two adjunctions \(L \dashv R \dashv K\), with both \(L : \mathbf {F} \to \mathbf {P}\) and \(K : \mathbf {F} \to \mathbf {P}\) fully faithful. From these two adjunctions, we have both an idempotent monad \(KR\) and an idempotent comonad \(LR\) on the category \(\mathbf {P}\). In the rest of this post, let's denote the monad \(KR\) by \(\bigcirc : \mathbf {P} \to \mathbf {P}\). Explicitly, its action on a profunctor \(P\) is \[ \bigcirc P(a, b) = (a \Rightarrow P(1, b)). \] The unit \(\eta _P : P \to \bigcirc P\) for this monad is \[ \eta _P(a,b)\;(p \in P(a,b)) = \lambda (x \in a).\; P(\lambda {*}.\; x, \mathrm {id}_b)(p). \] We call a profunctor \(P\) modal if the unit \(\eta _P : P \to \bigcirc P\) is an isomorphism. The full subcategory of modal profunctors is equivalent to \(\mathbf {F}\), so we can talk about things in \(\mathbf {F}\) without leaving the category \(\mathbf {P}\).

The coreflective adjunction \(L \dashv R\) also gives an idempotent comonad, but so far I have been only looking at the idempotent monad \(\bigcirc \) because of a crucial property of \(K : \mathbf {F} \to \mathbf {P}\): it preserves the substitution/composition monoidal products on \(\mathbf {F}\) and \(\mathbf {P}\).

The proof of \(K\) being strong monoidal is where we need the assumption that \(\mathbf {Set}_s\) is closed under \(\Sigma \)-types.

Consequently, for all \(P, Q \in \mathbf {P}\), we have \[ (\bigcirc P) \mathbin {\circ } (\bigcirc Q) = KRP \mathbin {\circ } KRQ \cong K(RP \otimes RQ). \] This means that composition of modal profunctors \((\bigcirc P) \mathbin {\circ } (\bigcirc Q)\) coincides with the substitution tensor \(RP \otimes RQ\) of their corresponding functors! This property is very useful because it means that we can talk about the monoidal category \((\mathbf {F}, \otimes , I)\) without leaving the monoidal category \((\mathbf {P}, \mathbin {\circ }, H)\) with the help of \(\bigcirc \).

In a similar vein, limits of modal profunctors coincide with the limits of their corresponding functors, because both \(K\) and \(R\) preserve limits (they are both right adjoints). For example, for all \(P,Q \in \mathbf {P}\) \[ (\bigcirc P) \times (\bigcirc Q) = KRP \times KRQ \cong K(RP \times RQ). \]

Unfortunately, we cannot say the same nice thing about colimits because \(K : \mathbf {F} \to \mathbf {P}\) does not preserve colimits in general, although \(R : \mathbf {P} \to \mathbf {F}\) does (because it is a left adjoint). This means that if we take the colimit \(\mathbf {Colim}_i \bigcirc P_i\) of a diagram of modal profunctors in \(\mathbf {P}\), it need not correspond to the colimit of the corresponding functors in \(\mathbf {F}\). For example, the coproduct \(\bigcirc P + \bigcirc Q\) in \(\mathbf {P}\) is \[ (a,b) \mapsto (a \Rightarrow P(1,b)) + (a \Rightarrow Q(1,b)), \] while if we take the coproduct of the corresponding functors in \(\mathbf {F}\) and embed it back in \(\mathbf {P}\) along \(K\), we obtain \[ (a, b) \mapsto a \Rightarrow (P(1, b) + Q(1,b)). \] Fortunately, this problem is easy to fix: if we want to take colimits of modal profunctors as functors, we first take the colimit in \(\mathbf {P}\) and then apply \(\bigcirc \) to it. Indeed, we have \[ \bigcirc (\mathbf {Colim}_i \bigcirc P_i) = KR(\mathbf {Colim}_i KRP_i) \cong K(\mathbf {Colim}_i RKRP_i) \cong K(\mathbf {Colim}_i RP_i). \] The first \(\cong \) is because \(R\) as a left adjoint preserves colimits. The second \(\cong \) uses the counit \(\epsilon : RK \to \mathrm {id}\) and the counit of a reflection adjunction is an isomorphism.

On some scratch paper I have checked that \(\bigcirc \) can be extended to a fibered modality, in the sense that we can define \(\bigcirc \) over every slice category of \(\mathbf {P}\) in a way that is stable under pullbacks. Moreover, if we have another sub-universe of \(\mathbf {Set}_l\) and lift it to a universe \(\mathcal {U} \in \mathbf {P}\) using Hofmann-Streicher lifting, we can internalise \(\bigcirc \) as a morphism \(\bigcirc : \mathcal {U} \to \mathcal {U}\). All this means that if we use Martin-Löf type theory as an internal language of \(\mathbf {P}\), the modality \(\bigcirc \) is very well behaved. It is simply a type former that works in every context; no Fitch-style locks needed.

However, I do not need dependent types for now, so I will leave the claims above for a future occasion. Also, if you know how the fiberedness of \(\bigcirc \) can be derived from some existing theorems in the literature, please let me know!

Finally I want to briefly talk about why I am interested in this \(\bigcirc \) thing. My motivation comes from this ongoing project of interpreting sophisticated data structures in various monoidal categories such as \((\mathbf {F}, \otimes , I)\) and \((\mathbf {P}, \mathbin {\circ }, H)\). I am especially interested in interpreting sequence-like data structures (lists, queues, finger trees, ...) in \((\mathbf {F}, \otimes , I)\), because their interpretation in this monoidal category would become data structures for abstract syntax trees, with potentially good time-complexities for operations such as variable substitution and pattern matching.

However, a significant difficulty with \((\mathbf {F}, \otimes , I)\) is that the substitution tensor \(\otimes \) is in general only distributive on one side: \[ (F + G) \otimes H \cong (F \otimes H) + (G \otimes H) \] but in general, \[ H \otimes (F + G) \not \cong (H \otimes F) + (H \otimes G). \] This means that the substructural internal language of \((\mathbf {F}, \otimes , I)\) (where the variables in a context are combined using \(\otimes \)) allows pattern matching of a variable \(x : F + G\) only when it is the first variable in a context. If \(\Gamma \) is non-empty, under the context \(\Gamma , x : F + G\), we cannot in general pattern match \(x\) because we do not have an isomorphism \[ \llbracket \Gamma \rrbracket \otimes (\llbracket F\rrbracket + \llbracket G\rrbracket ) \cong \llbracket \Gamma \rrbracket \otimes \llbracket F\rrbracket + \llbracket \Gamma \rrbracket \otimes \llbracket G\rrbracket . \]

This is a big restriction for programming in \((\mathbf {F}, \otimes , I)\) because many efficient data structures, such as finger trees and self-balancing binary trees, need to pattern match a variable before the variables preceding it are fully consumed.

On the other hand, the monoidal category \((\mathbf {P}, \mathbin {\circ }, H)\) does not have this problem: the tensor \(\mathbin {\circ }\) distributes over coproducts from both directions. Consequently, in the substructural internal language, we can pattern match coproducts as usual, and many familiar functional data structures (such as finger trees) can be implemented without any problem. The interpretation of sequence data structures in \((\mathbf {P}, \mathbin {\circ }, H)\) is exactly van der Ploeg and Kiselyov's type-aligned sequences.

Now, with the modality \(\bigcirc \), we can construct things for \(\mathbf {F}\) while working in the nicer category \(\mathbf {P}\). There should be some general theory for this, which I am still working on. For this post, I will just show you a concrete example. Fix an object \(A \in \mathbf {F}\) and suppose that we want to construct a representation of the free \(\otimes \)-monoid over \(A\) such that the associated operations are efficient. In particular, we want to find some \(X \in \mathbf {F}\) with operations: \[ v : I \to X,\ s : X \otimes X \to X,\ i : A \to X \] and co-operations: \[ p : X \to I + A \otimes X. \] One obvious solution for \(X\) is the list object \(\mu X.\; I + A \otimes X\) in \(\mathbf {F}\), but we would like a solution with better time-complexity for \(s : X \otimes X \to X\).

Now we rephrase this problem in the nicer world \((\mathbf {P}, \mathbin {\circ }, H)\). Our goal is to construct a modal object \(Y \in \mathbf {P}\) equipped with the following maps in \(\mathbf {P}\): \[ \begin {gathered} v : H \to Y,\ s : Y \mathbin {\circ } Y \to Y,\ i : KA \to Y, \\ p : Y \to \bigcirc (H + KA \mathbin {\circ } Y). \end {gathered} \] Note the \(\bigcirc \) in the codomain of \(p\), because coproducts in \(\mathbf {P}\) need to be reflected to become coproducts in \(\mathbf {F}\).

Without loss of generality, we can assume \(Y\) takes the form of \(\bigcirc Z\) for some (not necessarily modal) object \(Z \in \mathbf {P}\), equipped with maps: \[ \begin {gathered} v : H \to \bigcirc Z,\ s : \bigcirc Z \mathbin {\circ } \bigcirc Z \to \bigcirc Z, i : KA \to \bigcirc Z, \\ p : \bigcirc Z \to \bigcirc (H + KA \mathbin {\circ } \bigcirc Z). \end {gathered} \] By composing with the unit map \(Z \to \bigcirc Z\), to obtain \(v\) and \(i\), it is sufficient if we have \[ v' : H \to Z \quad \text {and}\quad i' : KA \to Z. \] Also, by using the functor action of \(\bigcirc \), for \(p\) it is sufficient if we have \[ p' : Z \to H + KA \mathbin {\circ } \bigcirc Z. \] To simplify \(s : \bigcirc Z \mathbin {\circ } \bigcirc Z \to \bigcirc Z\), we need the following result:

Because \(\bigcirc Z\) is modal, by this theorem we have \[ \bigcirc Z \mathbin {\circ } \bigcirc Z \cong \bigcirc Z \mathbin {\circ } \bigcirc (\bigcirc Z) \cong \bigcirc (Z \mathbin {\circ } \bigcirc Z). \] Consequently, to have a map \(s : \bigcirc Z \mathbin {\circ } \bigcirc Z \to \bigcirc Z\), it is sufficient to have \[ s' : Z \mathbin {\circ } \bigcirc Z \to Z. \] Now if we look at the types of the maps \(v', i', p'\), and \(s'\), we can see that \(Z\) is like a list object in \(\mathbf {P}\) except that the second argument of \(s'\) is protected by the modality \(\bigcirc \). A simple solution for this \(Z\) is \[ \mu Z.\; H + KA \mathbin {\circ } \bigcirc Z. \] But for better complexity, we can adapt Okasaki's catenable list from Chapter 10 of his famous book to work with \(\bigcirc \) too: \[ \mu Z.\; H + KA \mathbin {\circ } Q (\bigcirc Z), \] where \(Q : \mathbf {P} \to \mathbf {P}\) is any efficient implementation of queues on \(\mathbf {P}\) that supports: \[ \begin {gathered} H \to Q(\bigcirc Z) \\ Q(\bigcirc Z) \mathbin {\circ } \bigcirc Z \to Q(\bigcirc Z) \\ Q(\bigcirc Z) \to H + \bigcirc Z \mathbin {\circ } Q(\bigcirc Z). \end {gathered} \] As I mentioned in the last section, the crucial advantage of \(\mathbf {P}\) is that many efficient data structures can be used to implement queues in \(\mathbf {P}\), such as finger trees. This would then give us an efficient representation of \(Z\) where all four operations \(v', i', p', s'\) run in constant time. The original \(X \in \mathbf {F}\) is then \[ X = RZ = R(\mu Z.\; H + KA \mathbin {\circ } Q (\bigcirc Z)), \] whose Kleisli embedding is \(KX = \bigcirc Z\). This is how we obtain a construction for \(\mathbf {F}\) by making a detour to the nicer world of \(\mathbf {P}\).