To clarify #21:

> As Matthew tersely indicated, if a poset \$$A\$$ has binary meets, for each element \$$a \in A\$$ there's a monotone function
> $$a \wedge \cdot : A \to A$$
> sending each element \$$b \in A \$$ to \$$a \wedge b\$$. Sometimes all these monotone functions have right adjoints, which we denote by
> $$a \to \cdot : A \to A$$
> which send each \$$c \in A\$$ to \$$a \to c \$$. As I explained in comment #13, this occurs iff
> $$a \wedge b \le c \textrm{ if and only if } a \le (b \to c)$$
> for all \$$a,b,c \in A\$$. Or in words, "\$$a \wedge b\$$ implies \$$c\$$" if and only if "\$$a\$$ implies \$$b \to c \$$".

The latter condition actually shows that \$$(\wedge b)\$$ and \$$(b \to)\$$ are adjoint, correct? (Of course, \$$\wedge\$$ is commutative.) We didn't actually use the \$$(a \wedge)\$$ and \$$(a \to)\$$ introduced prior.

It seems like the chain \$$\Delta \dashv \, \wedge \dashv\, \to\$$ is a little bit fictitious. By which I mean, \$$\wedge\$$ is simultaneously denoting two different species: a binary operator and a family of unary operators, the former of which might not have a right adjoint, and the latter of which might not have left adjoints.