Hey John,

Thanks for clearing up my confusion regarding \$$f_\ast\$$!

> I'll sketch a strategy to define it in terms of a _right_ adjoint.
>
> We can think of "complement" in logical terms as "negation". To define "negation" in a fairly general poset, I might try to use a few facts:
>
> * The [material conditional](https://en.wikipedia.org/wiki/Material_conditional) \$$a \to b\$$ - that is, the proposition _in our poset_ that means "\$$a\$$ implies \$$b\$$" - can be defined in terms of a right adjoint, since
>
> $$x \wedge a \implies b \textrm{ if and only if } x \implies (a \to b)$$

This is what Joel Jennings was saying in [#8](https://forum.azimuthproject.org/discussion/comment/16680/#Comment_16680).

This isn't *classical logic*, though. It's a sublogic called *intuitionistic logic*. I was pioneered by L. E. J. Brouwer in his paper [*The Unreliability of the Logical Principles* (1908)](https://arxiv.org/pdf/1511.01113.pdf). In this paper he rejects the [*law of the excluded middle*](https://en.wikipedia.org/wiki/Law_of_excluded_middle):

$$a \vee \neg a$$

If we define \$$\neg a := a \to \bot\$$, we end up with posets where this isn't true.

**Maybe we don't want it to be true**! You can use it to make rather disappointing proofs, as Brouwer argues. Also, I can't write a program in Haskell with type signature p :: Either (a -> _|_) a.

I argued that if you have a lattice \$$(P, \leq, \wedge, \vee, \to, \bot)\$$ we can always construct a sublattice with domain \$$\bar{\bar{P}} \subset P\$$ where the excluded middle works again. This is done by closing over every element with the closure operator \$$\neg (\neg\ \cdot)\$$. This is *Glivenko's Theorem*. Since \$$a \leq \neg (\neg a)\$$, then \$$\neg (\neg\ \cdot)\$$ is a *monad*, as you hinted in your puzzle in [lecture 4](https://forum.azimuthproject.org/discussion/comment/16320/#Comment_16320).