Is there an extension of the covariant powerset functor to Rel that agrees with its definition on Set?

45 Views Asked by At

Is there an extension of the covariant powerset functor to $\mathbf{Rel}$ that both agrees with its definition on $\mathbf{Set}$, and preserves the dagger involution on $\mathbf{Rel}$?

Relations are like functions, but more symmetrical: they behave the same with respect to inputs and outputs. I'm trying to understand whether there is a relational extension of the idea of "mapping a function over a set" that is symmetrical in this way. I'm using "mapping" here in the programming sense of applying something to every element of a set.

We have the covariant powerset functor $P: \mathbf{Set} \rightarrow \mathbf{Set}$, which maps a function over sets: For $f: X \rightarrow Y$,

$$P(f): P(X) \rightarrow P(Y)$$ $$P(f)(A) = \{f(a) \,|\, a \in A\}$$

We could also say that $P(f)$ sends sets to their images under $f$. The idea of images is not exclusive to functions, it also applies to relations; so we can define another functor $P_{RF}: \mathbf{Rel} \rightarrow \mathbf{Set}$ that sends sets to their images under a relation. For $R \subseteq X \times Y$,

$$P_{RF}(R): P(X) \rightarrow P(Y)$$

$$P_{RF}(R) (A) = \{y \; | \; \exists a \in A, a R y \}$$

However, this functor treats inputs and outputs differently: it's a functor to $\mathbf{Set}$, not $\mathbf{Rel}$. Even if we think of $\mathbf{Set}$ as a subcategory of $\mathbf{Rel}$ using the functor $Graph: \mathbf{Set} \hookrightarrow \mathbf{Rel}$, we have that

$$Graph(P_{RF}(R^\dagger)) \neq Graph(P_{RF}(R))^\dagger$$

What I'm wondering is: is there a functor $P_{RR} : \mathbf{Rel} \rightarrow \mathbf{Rel}$ such that

$$P_{RR} \circ Graph = Graph \circ P$$ and $$P_{RR}(R^\dagger) = P_{RR}(R)^\dagger$$ ?