About Coreader Comonads

Question

Here [1] we see a paper that describes when you can compose a directed container over distribution monads.

Here is their definition of a directed container

Here is their definition of the coreader comonad.

A directed container will have a kind of graph structure. For instance, consider the nonempty list comonad. Lists are just chains with a head and tail so the graph starts us just chains. So $S$ is just lists.

What I am wondering about is what is the graph structure of the coreader comonad seen as a directed container? In particular, I want to know if the graph structure resembles a complete lattice, and hence a dcpo. What are the restrictions on the set $S$? For instance, in the binary tree directed container, S is literally binary trees. What kinds of shapes, $s$, admit a coreader comonad? What are some examples of coreader commands where we are interested in interesting shapes $S$? Can we just outright say that $S$ is the set of all dcpos? Is it possible the positions $P(S) = \{ \top \}$ are the least upper bounds for each dcpo in $S$?

Edit

The coreader comonad is related to the quantum reader monad. This reader is then based on the complete lattice of protection operators on a hilbert space. There seems to be something non-trivial to my idea.

[1] Karamlou, Amin, and Nihil Shah. "No Go Theorems: Directed Containers That Do Not Distribute Over Distribution Monads." Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science. 2024.

Answer 1

It seems that the definition of a directed container in the linked paper just says that a directed container is a category. In more detail a directed container consists of:

• A set $S$
• For each $s\in S$, a set $P(s)$ and an element $o_s\in P(s)$
• For each $p\in P(s)$, an element $s\downarrow p\in S$
• For each $p'\in P(s\downarrow p)$, an element $p\oplus_sp'\in P(s)$
• Subject to certain axioms.

These axioms just mean we have a category $\mathcal{C}$ with $\operatorname{obj}(\mathcal{C})=S$, where $\mathcal{C}(s,t)=\{p\in P(s):s\downarrow p=t\}$, and composition is given by $p'\circ p=p\oplus_sp'$.

Given a set $X$ we can define $GX=\coprod_s\prod_t\operatorname{Map}(\mathcal{C}(s,t),X)$. We define $\epsilon\colon GX\to X$ by $\epsilon(u)=u_s(1_s)$ for $u\in\prod_t\operatorname{Map}(\mathcal{C}(s,t),X)\subseteq GX$. For such $u$ we also define $\delta(u)\in\prod_t\operatorname{Map}(\mathcal{C}(s,t),GX)\subseteq G^2X$ as follows. For any $m\in\mathcal{C}(s,t)$, the element $\delta(u)_t(m)$ wil lie in the subset $\prod_r\operatorname{Map}(\mathcal{C}(t,r),X)\subseteq GX$, and will be given by $\delta(u)_t(m)_r(n)=u(n\circ m)$ for all $n\in\mathcal{C}(t,r)$. This is the natural description of the comonad associated to a directed container.

We can regard $\mathbb{N}$ as a category, with a single morphism from $s$ to $t$ when $s\geq t$. The associated comonad $G$ is then the nonempty list comonad.

We can regard any set $S$ as a category with only identity morphisms. The associated comonad is then the coreader comonad.

It seems that the binary tree example can be formulated as follows. Let $B_\infty$ be the standard infinite binary tree, say with vertex set $\mathbb{N}^+$, where the left branch of $n$ is $2n$ and the right branch is $2n+1$. We regard this as a partially ordered set with the root at the bottom. For any $a\in B_\infty$ there is an evident inclusion $f_a\colon B_\infty\to B_\infty$ sending the root to $a$. By a binary tree we mean a finite subset $T\subseteq B_\infty$ containing the root and closed downwards. For such $T$ and $a\in T$ we put $T/a=\{t:f_a(t)\in T\}$, so $f_a$ gives an isomorphism from $T/a$ to $\{x\in T: x\geq a\}$. We can regard the set $\mathcal{C}$ of binary trees as a category with $\mathcal{C}(T_0,T_1)=\{a\in T_0:T_0/a=T_1\}$. Then $\coprod_{T_1}\mathcal{C}(T_0,T_1)=T_0$, so the associated comonad is $GX=\coprod_{T_0}\operatorname{Map}(T_0,X)$.

The original question is not very clear, but it appears to be asking about a poset or lattice structure on $S$ arising from the directed container structure. The answer seems to be that in general we have a category structure, which can be regarded as a poset structure only if the morphism sets are subsingletons. However, the category structure can be arbitrary.