John wrote:

> **Puzzle.** Suppose \$$X\$$ and \$$Y\$$ are preorders. Can we reinterpret a feasibility relation, namely a monotone function
>
> $\Phi : X^{\text{op}} \times Y \to \textbf{Bool} ,$
>
> as a monotone function
>
> $\hat{\Phi} : X^{\text{op}} \to \textbf{Bool}^{\textbf{X}}$
>
> or perhaps slightly better
>
> $\tilde{\Phi} : Y \to \textbf{Bool}^{\textbf{X}^{\text{op}}} ?$
>
> The first problem here is figuring out what's an exponential of preorders!

Okay, I cheated a little and I looked this up in [Steve Awodey's lecture notes](https://www.andrew.cmu.edu/course/80-413-713/notes/chap06.pdf).

If \$$X\$$ and \$$Y\$$ are posets, then let \$$Y^X\$$ be the set \$$\lbrace F: X \to Y \mid F \text{ is monotone}\rbrace\$$. If \$$f,g \in Y^X\$$ then \$$f \leq\_{Y^X} g\$$ if and only if \$$f(x) \leq\_Y g(x)\$$ for all \$$x \in X\$$.

We want to show \$$\mathrm{Hom}(X\times Y,Z) \cong \mathrm{Hom}(X,Z^Y)\$$. This can be done by defining

- \$$\mathtt{curry} : \mathrm{Hom}(X\times Y,Z) \to \mathrm{Hom}(X,Z^Y)\$$ and
- \$$\mathtt{uncurry} : \mathrm{Hom}(X,Z^Y) \to \mathrm{Hom}(X\times Y,Z)\$$

We also need to show these definititions are well defined, and demonstrate \$$\mathtt{curry} \circ \mathtt{uncurry} = id\$$ and \$$\mathtt{uncurry} \circ \mathtt{curry} = id\$$.

Here are the definitions:

\begin{align} \mathtt{curry}(f) & := x \mapsto (y \mapsto f (x,y))\\\\ \mathtt{uncurry}(g) & := (x,y) \mapsto (g(x))(y) \end{align}

Let's check that if \$$f : X \times Y \to Z\$$ is a monotonic function then \$$\mathtt{curry}(f) : X \to Z^Y\$$ is monotonic.

First, let \$$x \leq x'\$$. We need to show \$$\mathtt{curry}(f)(x) \leq \mathtt{curry}(f)(x')\$$. But this means we need to show \$$\mathtt{curry}(f)(x)(y) \leq \mathtt{curry}(f)(x')(y)\$$ for all \$$y\$$. By evaluating these functions we can see we want to show \$$f(x,y) \leq f(x',y)\$$ for all \$$y\$$. Since \$$x \leq x'\$$ we know that \$$(x,y) \leq (x',y)\$$ by definition of the product order, and \$$f(x,y) \leq f(x',y)\$$ since \$$f\$$ is mono.

Next, we'll want to check if \$$g : X \to Z^Y\$$ is a monotonic function then \$$\mathtt{uncurry}(g) : X \times Y \to Z\$$ is monotonic.
Let \$$(x,y) \leq (x',y')\$$. We need to show \$$\mathtt{uncurry}(g)(x,y) \leq \mathtt{uncurry}(g)(x',y')\$$. This amounts to showing if \$$x \leq x'\$$ and \$$y \leq y'\$$ then \$$(g(x))(y) \leq (g'(x'))(y')\$$. We know that \$$g(x') \in Z^Y\$$, are monotonic by definition, hence \$$(g(x'))(y) \leq (g(x'))(y')\$$. We also know that \$$g\$$ is monotonic, hence \$$g(x) \leq g(x')\$$, and thus \$$g(x)(y) \leq g(x')(y)\$$. By transitivity we have \$$(g(x))(y) \leq (g(x'))(y')\$$.

We can be confident then that \$$\mathtt{curry}\$$ and \$$\mathtt{uncurry}\$$ are well defined.

Next, let's check that they are inverses. Evaluating the functions defined gives:

\begin{align} (((\mathtt{curry} \circ \mathtt{uncurry})(g))(x))(y) & = ((\mathtt{curry} (\mathtt{uncurry}(g)))(x))(y) \\\\ & = (\mathtt{uncurry}(g))(x,y) \\\\ & = (g(x))(y) \end{align}

However, \$$((id(g))(x))(y) = (g(x))(y)\$$, so by [*extensionality*](https://en.wikipedia.org/wiki/Axiom_of_extensionality) we have \$$(\mathtt{curry} \circ \mathtt{uncurry}) = id\$$. Extensionality is the principle that says that if two sets have the same elements, then they are equivalent. In Higher Order Logic and the [λ-calculus](https://en.wikipedia.org/wiki/Lambda_calculus#%CE%B7-conversion), it holds that if two functions are the same on all inputs then they are the same.

Considering the other direction, we have:

\begin{align} ((\mathtt{uncurry} \circ \mathtt{curry})(g))(x,y) & = ((\mathtt{curry}(g))(x))(y) \\\\ & = g(x,y) \end{align}

Hence, we have the isomorphism we desire.

We can note that the category of Posets and the category of Preorders have a terminal object: the poset with 1 element. So the categories are in fact [Cartesian Closed Categories](https://en.wikipedia.org/wiki/Cartesian_closed_category).

They also have coproducts (I can talk about this a little if someone wants). I do not know if they have an initial object, however. So I can't say if the categories of Posets and Preorders are [Bicartesian closed](https://en.wikipedia.org/wiki/Cartesian_closed_category#Equational_theory)...