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^+\\).

The *left adjoint* given by:

$$
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\\)