Here is another comment somewhat tangential to Mike's post about distributivity. If a lattice is completely distributive, CD, then the fact that the opposite distributivity holds might be written AC==>(CD<==>CD^op), for at least some aspect of choice seems to be necessary. Write CCD, "constructive complete distributivity", for the apparent weakening of CD that requires distributivity, in the sense Mike posted, of infs over sups of down-closed subsets. Then AC<==>(CD<==>CCD). On the other hand, writing BOO for the axiom which states that the object of truth values is Boolean, one has BOO<==>(CCD<==>CCD^op). Combining these results gives an indirect proof of AC==>BOO. The fact that BOO is necessary for CCD<==>CCD^op is, at first, surprising. The equivalence of CCD and CCD^op rests entirely on whether or not the object of truth values, which is always CCD, is CCD^op. In set^2, the object of truth values being 3--->2, one expects a counterexample to the claim. The pitfall here is that distributivity of binary sup over binary inf does not extend to distributivity of sups over infs of up-closed subobjects. To sketch a proof of the necessity of BOO, show that CCD==>HEY. Unlike the situation for general Heyting algebras, it follows from a lemma attributed to both Benabou and Reyes that if the opposite of the object of truth values is Heyting then it is Boolean. These observations are simplified by the fact that CCD(L) is equivalent to the statement that sup:DL--->L has a left adjoint, where DL is the lattice of down-closed subobjects of L, and DL is equivalent to ord(L^op, Omega), where Omega is the object of truth values. RJ