Return to Answer

Edit: Will Sawin has pointed out some difficulties with this answer. I'm going to leave this up for at least a while, in case anyone has any ideas about repairing it. Or perhaps this could be a cautionary tale?

Officially, a sup-lattice is a $\mathbf{P}$-algebra. It can also be described as a poset $X$ whose Yoneda embedding $y_X: X \to \mathbf{P}X$ has a left adjoint (which will then be the algebra structure $\mathbf{P}X \to X$: there can be only one, as $\mathbf{P}$ is a lax idempotent or KZ monad).

Proof: It suffices to check this at the level of underlying sets, by concreteness of $\text{Choq}$ over $\text{Set}$. Let $U \in \mathbf{P}A$ be a down-set of $A$. Then $\mathbf{P}h(U) = \{b \in B: \exists_{a \in A} a \in U \wedge b \leq h(a)\}$. The function $[h^{op}, \Omega]$ sends this down-set to $\{a' \in A: \exists_{a \in A} a \in U \wedge h(a') \leq h(a)\}$. Since $h$ is an embedding, this is the same as $\{a' \in A: \exists_{a \in A} a \in U \wedge a' \in a\}$, but this is just $U$ since $U$ is downward-closed. $\Box$

Officially, a sup-lattice is a $\mathbf{P}$-algebra. It can also be described as a poset $X$ whose Yoneda embedding $y_X: X \to \mathbf{P}X$ has a left adjoint (which will then be the algebra structure $\mathbf{P}X \to X$: there can be only one, as $\mathbf{P}$ is a lax idempotent or KZ monad).

Proof: It suffices to check this at the level of underlying sets, by concreteness of $\text{Choq}$ over $\text{Set}$. Let $U \in \mathbf{P}A$ be a down-set of $A$. Then $\mathbf{P}h(U) = \{b \in B: \exists_{a \in A} a \in U \wedge b \leq h(a)\}$. The function $[h^{op}, \Omega]$ sends this down-set to $\{a' \in A: \exists_{a \in A} a \in U \wedge h(a') \leq h(a)\}$. Since $h$ is an embedding, this is the same as $\{a' \in A: \exists_{a \in A} a \in U \wedge a' \leq a\}$, but this is just $U$ since $U$ is downward-closed. $\Box$

Proof: Regard $X$ as an internal discrete poset (both maps of the span being $1_X$). There is an evident identification $P(L \times X) = P(L)^X$. Now examine the diagram

Proof: Regard $X$ as an internal discrete poset (both maps of the span being $1_X$). There is an evident identification $\mathbf{P}(L \times X) = (\mathbf{P}L)^X$. Now examine the diagram