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.

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