Dan noted in a Lecture 26
that John switched the unit conditions for lax and oplax in this Lecture. Here is his post:
I was having a hard time proving [puzzle 83](https://forum.azimuthproject.org/discussion/2098/lecture-27-chapter-2-adjoints-of-monoidal-monotones#latest)
and I think it's because the unit conditions are the other way around for the lax and oplax monotones, respectively:
> - For the lax monotone we should require:
\\( I_Y \le f(I_X) . \\)
> - For the oplax monotone we should require:
\\( f(I_X) \le_Y I_Y . \\)
> And a nitpick:
> one of these equations was using \\(1\\) rather than \\(I\\) to denote the unit;
I've noticed this notation is also mixed at the end of the [next lecture](https://forum.azimuthproject.org/discussion/2098/lecture-27-chapter-2-adjoints-of-monoidal-monotones#latest).
For reference we have
- **Lecture 26** Lax: \\(f(I_X) \le_Y I_Y\\). Oplax: \\(I_Y \le_Y f(I_X) \\).
- **Lecture 27** Lax: \\(I_Y \le_Y f(I_X) \\). Oplax: \\(f(I_X) \le_Y I_Y\\).
My examples and proofs seem to disagree with each other about what the condition *should* be. Here's what I've tried so far:
**An example showing that the condition Lecture 26 should be true:**
Define \\(f: \mathbb Z \to \mathbb R\\) by \\(f(x) = x+ 1\\). It has a right adjoint \\(g: \mathbb R \to \mathbb Z\\) defined by \\(g(y) = \lfloor y-1 \rfloor\\). So \\[g(0) = -1 \leq 0.\\] Since the super-theorem wants \\(g\\) to be lax monoidal monotone, the unit condition for lax monoidal monotone should be \\(g(I_Y) \leq_X I_X\\) which is the condition John listed in Lecture 26.
**A hand-wavy reason why the Lecture 26 condition should be true:**
Again, I'm trying working to define the condition so that the super-theorem is true. If \\(g\\) is a right adjoint that means it is the approximate inverse of \\(f\\) from below. A perfect inverse would map \\(I_Y\\) exactly to \\(I_X\\) so since \\(g\\) is "from below" if makes sense that \\(g(I_Y) \leq_X I_X\\).
**Why it would be nice if the condition in Lecture 27 were true:**
I agree with Dan that the Lecture 26 condition seems much more challenging to prove than the Lecture 27 condition: \\(I_X \leq_X g(I_Y) \\). If this is the unit condition, then it can be proved in the super-theorem as follows: By hypothesis \\(f\\) is oplax so by the Lecture 27 oplax unit condition \\(f(I_X) \leq_Y I_Y\\). Since \\(f\\) is left adjoint to \\(g\\) this implies that \\(I_X \leq_X g(I_Y)\\).
I feel like I've got myself all tangled up! What do you all think?