it occurs to me that i have been preaching the helpfulness of the well-ordering of all data in the world, as demonstrated by its utility to the programmers --- and i totally forgot to mention its utility as a *categorical structure*!! i forgot to plug my own work which provides the categorical underpinning for the well-ordering sermon...
so we all love the **cartesian closed categories**, characterized by the adjunction
CC(XxA,B) ~ CC(X, A=>B) (*)
but the cccs are *extensional* universes, corresponding to the extensional type theories. if we want to capture the world with actual programs, say in a programming language P, then we have just a family of X-natural surjections
CC(XxA,B) <<--- CC(X, P) (#)
the surjections say that every computably X-indexed family of computable functions from A to B can be programmed by a computably X-indexed family of programs in P. since computable functions don't always halt, we cannot avoid at least the computational effect of nontermination, and the AxB is not a product but a tensor, say from a commutative computational monad. such (symmetric) monoidal categories with a "programming language" type P and natural surjections (#) is what i called *monoidal computers*, because you can program everything using (#), without ever saying anything else about the programming language. it is turing complete. it's all spelled out in my book.
but the snag is that (*) is a *property* of a category, whereas (#) is a structure. a category can be cartesian closed in only one way, but it can be a monoidal computer in many ways. one is tempted to say that this is unavoidable since the CT thesis leaves us with many models of computation and infinitely many unnatural isomorphisms between any two.
**** enter the well-order ****
IF you remember that programming languages are well-ordered, and assume that the type P carries a well-ordering,
THEN (#) becomes a *property*. a monoidal category CC can have at most one well-ordered type P with (#), up to isomorphism.
the nices thing is that you prove this by spelling out what came to be called the cantor-bernstein theorem, but in cantor's way: using the well-order. (dedekind discouraged publishing this because the well-ordering of the reals was cantor's by far the deadliest mortal sin. even now, to really keep the reals well-ordered you need something like levin's dovetailing approximations...)
anyway, this proof is in Ch 8 of my book *programs as diagrams*. computability is a *categorical property* --- IF you take into account that the programming language is well-ordered (which implies that all checkable types are).
sorry about plugging my book. i know it's a world of tweets and advertising campaigns but i still feel bad. my alibi is that the fact that computability+well-order is a categorical property is way more important than any book and surely goes deeper than i can comprehend no matter how many turing degrees and oracles i consult...
(can't believe that i only remembered to mention this after like 5 posts...)
-- dusko