Keith: currying \\(A \cong A^\mathbf{1}\\) gives \\(A \times \mathbf{1} \cong A\\), not \\(A \times \mathbf{1} \cong A^\mathbf{1}\\). Remember,

\[ A \times B \cong C \text{ iff } A \cong C^B \]

So, if have all these tools at our disposal, \\(A \cong A^\mathbf{1}\\) instantly implies what we want.

But more importantly: your proof has just reduced showing \\(A \times \mathbf{1} \cong A\\) to showing \\(A \cong A^{\mathbf{1}}\\) and showing that currying works for preorders. These facts take more work to prove than proving \\(A \times \mathbf{1} \cong A \\) directly!

I notice that you often seek 'tricks' rather than just straightforwardly working from the definitions. This is sometimes a virtue, but also sometimes a vice. When one is getting started in a new subject, there are always lots of things one needs to prove by just straighforwardly manipulating the definitions. It's important to develop the confidence and 'muscle' to push one's way through these jobs.

In our situation here, I've defined products of preorders, but not exponentials of preorders, and I haven't proved that

\[ A \times B \cong C \text{ iff } A \cong C^B . \]

So, a proof that relies on these not-yet-established facts doesn't count as a proof. Part of the game of math is figuring out how to get from what we officially 'have' to what we're trying to prove. We don't have the tools you're trying to use. It's as if I said "okay, let's build our strength and endurance: climb that hill!" and you said "I'll just get into my helicopter..." It's missing the point of the exercise.

For example: we've discussed exponentials of categories, which I called 'functor categories', but we haven't proved \\( A \times B \cong C \text{ iff } A \cong C^B \\) for these; nor have we proved that the exponential of categories that happen to be preorders is again a preorder, etc. All this stuff is _true_, but it's about fifty times faster to prove \\( A \times \mathbf{1} \cong A \\) _directly_, than to prove all this stuff.

In fact, I could have proved it in much less time than it took to write this comment! I'm only writing it because I want to help you develop 'muscle' as well as cleverness.

\[ A \times B \cong C \text{ iff } A \cong C^B \]

So, if have all these tools at our disposal, \\(A \cong A^\mathbf{1}\\) instantly implies what we want.

But more importantly: your proof has just reduced showing \\(A \times \mathbf{1} \cong A\\) to showing \\(A \cong A^{\mathbf{1}}\\) and showing that currying works for preorders. These facts take more work to prove than proving \\(A \times \mathbf{1} \cong A \\) directly!

I notice that you often seek 'tricks' rather than just straightforwardly working from the definitions. This is sometimes a virtue, but also sometimes a vice. When one is getting started in a new subject, there are always lots of things one needs to prove by just straighforwardly manipulating the definitions. It's important to develop the confidence and 'muscle' to push one's way through these jobs.

In our situation here, I've defined products of preorders, but not exponentials of preorders, and I haven't proved that

\[ A \times B \cong C \text{ iff } A \cong C^B . \]

So, a proof that relies on these not-yet-established facts doesn't count as a proof. Part of the game of math is figuring out how to get from what we officially 'have' to what we're trying to prove. We don't have the tools you're trying to use. It's as if I said "okay, let's build our strength and endurance: climb that hill!" and you said "I'll just get into my helicopter..." It's missing the point of the exercise.

For example: we've discussed exponentials of categories, which I called 'functor categories', but we haven't proved \\( A \times B \cong C \text{ iff } A \cong C^B \\) for these; nor have we proved that the exponential of categories that happen to be preorders is again a preorder, etc. All this stuff is _true_, but it's about fifty times faster to prove \\( A \times \mathbf{1} \cong A \\) _directly_, than to prove all this stuff.

In fact, I could have proved it in much less time than it took to write this comment! I'm only writing it because I want to help you develop 'muscle' as well as cleverness.