Hey John,

Thanks for clearing up my confusion regarding \\(f_\ast\\)!

In [#34](https://forum.azimuthproject.org/discussion/1931/lecture-9-adjoints-and-the-logic-of-subsets#latest) you wrote:

> 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).