David Feldman <david.feldman@unh.edu> asked about the distributive law for Set. As he points out, distributivity lies somewhere between simply having products and coproducts in a category, and being a topos. I shall be very didactic about the former, but at the end is a new point of research about the latter. Robin Cockett wrote about distributive categories in "Mathematical Structures in Computer Science" in 1993. He and Robert Seely are the experts on this, and also have a more recent paper in TAC (tac.mta.ca/tac). I would urge any mathematical student who hasn't done so already to compute the products and coproducts in the categories of sets, groups, Abelian groups and commutative rings. These illustrate when distributivity and its dual succeed or fail. See Section 5.4 of my book "Practical Foundations of Mathematics" for a survey of these examples, http://www.dcs.qmul.ac.uk/~pt/book/html/s54.html Likewise, I would urge computer science students to compute the products and coproducts in the categories of monoids and commutative monoids. (These are very different!) Section 2.3 of my book gives the type theoretic rules for products and sums. It is easy to find (two equal expressions for) a map (Gamma x Y) + (Gamma x N) --> Gamma x (Y+N) (they're on p275 of my book). The other way is more difficult. (I think David got this the wrong way round, but I don't have to hand an example of a category in which there is no such map at all.) We can already see the point in propositional logic. The following proof box appears in Lemma 1.6.3 (p37). Unfortunately, it was messed up in the original 1999 printing, but corrected in the 2000 reprint. 1 G data 2 Y or N data --------------------------------------------------------------------- 3 | Y hypothesis | N hypothesis | 4 | G (1) | G (1) | 5 | G and Y and-I(3,4) | G and N and-I(3,4) | 6 | (G and Y) or (G and N) or-I0(5) | (G and Y) or (G and N) or-I1(5) | --------------------------------------------------------------------- 7 (G and Y) or (G and N) or-E(2) The point is that Gamma is IMPORTED into the box in line 4. What's this got to do with categorical notation? The box style means that we have (implicit terms of) the types shown, in the context that consists of the global DATA and the local HYPOTHESES. Since the local context of a mathematical argument varies more slowly than its local conclusions, boxes allow us to concentrate on the local conclusions, but read off the context from the whole presentation. The categorical jargon for "contexts" and "conclusions" (or "types") is "domain" and "codomain" respectively, or you may prefer "source" and "target". So the left half of lines 4 and 5 say that we have map Gamma x (Y+N) --> Gamma x Y --> (Gamma x Y) + (Gamma x N) and the universal property of the coproduct is captured in line 7, where we put this together with its twin from the right. The "distributivity" property of the category of sets is much better than that in propositional logic, because Y+N is the "disjoint union". This property has been called "extensivity", and Steve Lack is the technical expert on it. See Section 5.5 of my book for my version. Topological spaces, locales, PREdomains and algebraic varieties also form extensive categories. (Locales and algebraic varieties are the names given to the opposites of the categories of frames and of commutative rings, with their respective homomorphisms.) Exercise 5.31 gives a hint at the proof of extensivity for locales and algebraic varieties. It makes use of the algebra - addition and multiplication - in the OPPOSITE category. In 1974, when elementary toposes were first being developed, Bob Pare' showed that the contravariant powerset on any topos makes its opposite the category of algebras for a monad. This is an intuitionistic version of a classical theorem of Lindenbaum and Tarski, which we state in categorical terms as the dual equivalence between sets and complete atomic Boolean algebras. Pare''s theorem may instead be taken as an axiom, with powers of ANY object Sigma that has them, in place of the contravariant powerset. This is the basic idea behind my "Abstract Stone Duality" programme, http://www.di.unito.it/~pt/ASD Here is the new point of research: assuming only that the self-adjoint functor Sigma^(-) is monadic, and that Sigma has a constant 1-->Sigma, then the category is extensive. This is proved in the final section of "Subspaces in Abstract Stone Duality", which you can get from the ASD web page. Paul <pt@di.unito.it> but physically in London.