First off, kudos to Alex and Owen! These are some great problems and solution is super insightful.

@ John Baez

Following Owen's response [here](https://forum.azimuthproject.org/discussion/comment/16673/#Comment_16673), it's not necessary to demand a total order on \$$\leq\$$.

Please correct me if I am mistaken, but it suffices to demand that \$$\leq\$$ have *immediate predecessors* (for the right adjoint).

Dually, to solve AV3, we should demand that \$$\leq\$$ have *immediate successors*. That is, there's a successor operation \$$(\cdot)^+ : A \to A\$$ such that for all \$$x\$$ that \$$x > y\$$ if and only if \$$x \geq y^+\$$.

$$l(y,z) = \begin{cases}y & \text{if }y\geq z\\\\y^+& \text{otherwise}\end{cases}$$

(it's just the same as the right adjoint with successor swapped for processor and the order flipped)

**Proof**.

This proof closely follows Owen's original proof [here](https://forum.azimuthproject.org/discussion/comment/16673/#Comment_16673).

We require that \$$l\$$ satisfy the following law:

$$\begin{eqnarray} l(y,z) \leq_A x & \Longleftrightarrow & (y,z) \leq^{lex} (x,x) \\\\ & \Longleftrightarrow & (y,z) <^{lex} (x,x) \text { or } (y,z) = (x,x) \\\\ & \Longleftrightarrow & y <_A x \text{ or } (y = x \text{ and } z <_A x) \text { or } (y,z) = (x,x) \end{eqnarray}$$

Consider the case where \$$y = z\$$. Then \$$l(y,z) = l(y,y)\$$, and

$$\begin{eqnarray} l(y,y) \leq_A x & \Longleftrightarrow & y <_A x \text{ or } (y = y \text{ and } y <_A x) \text { or } (y,y) = (x,x) \\\\ & \Longleftrightarrow & y \leq_A x \end{eqnarray}$$

Which is satisfied since \$$l(y,y) = y\$$ by definition.

Next consider when \$$y > z\$$. Then \$$y = x \text{ and } z <_A x\$$ is equivalent to \$$y = x\$$ and \$$(y,z) \neq (x,x)\$$, so:

$$\begin{eqnarray} l(y,z) \leq_A x & \Longleftrightarrow & y <_A x \text{ or } (y = x \text{ and } z <_A x) \text { or } (y,z) = (x,x) \\ & \Longleftrightarrow & y <_A x \text{ or } y = x \\ & \Longleftrightarrow & y \leq_A x \end{eqnarray}$$

Which again is satisfied since \$$l(y,z) = y\$$ when \$$y > z\$$.

Finally assume \$$y \not\geq z\$$, then \$$y = x \text{ and } z <_A x\$$ and \$$(y,z) = (x,x)\$$ are always false, so \$$l(y,z) \leq_A x \Longleftrightarrow y <_A x\$$. But we know that \$$y^+ \leq_A x \Longleftrightarrow y <_A x\$$ for all \$$x\$$, so \$$l(y,z) = y^+\$$ is the right answer here.

\$$\Box\$$