On Jul 9, 2010, at 5:46 PM, Kevin Quick wrote:
That's probably an interesting assertion that one of the category theorists around here could prove or disprove. ;-)
It's not too hard. I don't like thinking about it in terms of category theory, though. It's easier to think about it in terms of universal quantification. The assertion is equivalent to the claim that (forall x, forall y, P x y) iff (forall y, forall x, P x y), though you have to do quite a bit of packing and unpacking to get there.
Another way to see it is in terms of recursion on initial algebras. Given an initial algebra A, and an initial algebra B, we'll say that A -> B represents the construction of attaching a copy of B to every element of A. We can assume that A and B are disjoint, because we can find a normal form A' -> B' for which A' and B' are disjoint, and such that A -> B is isomorphic to A' -> B'. (To see that, assume that some subalgebra C is contained in both A and B. Attaching a copy of B to every element of A means attaching a copy of C to each element, and also B \ C. But A already contains C. So A -> B is isomorphic to A - > B \ C). Note that since we can assume A and B are disjoint, we can also assume A and B are NOT mutually recursive. We can always find a way to break that mutual recursion up.
I'm not sure how to prove that A -> B and B -> A, as I defined them, are isomorphic. But they are. I guess we can re-interpret A and B as meet semi-lattices, and A -> B and B -> A as their products.
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
