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

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