Paul Levy writes ...a model of intuitionistic logic is a *bi*cartesian closed category. I see no reason to regard disjunction as more "peripheral" to intuitionistic logic than implication. (And, likewise, no reason to regard sum types as more peripheral to simple type theory than function types.) Does anybody disagree? The original intuitionists did, of course, see such reasons. But for those who don't care about such issues as the nature of mathematical existence there's this reason: if by a *bi*cartesian closed category one were to mean a ccc category whose dual is also ccc then one would be stuck with that fact that all *bi*cartesian closed categories are just pre-ordered sets. The status of disjunction and sum types in the presence of function types is, indeed, significantly different from the status of conjunction and products types. Let me take the occasion to record a factoid I don't think I ever had an excuse to record before (and don't really have one now). Define the notion of a Heyting semi-lattice (HSL) by removing disjunction and bottom from the definition of Heyting algebra. Define a _linear_ HSL as one that satisfies the further equation ((x -> y) -> z) ^ ((y -> x) -> z) = z e.g. any linearly ordered set with top (indeed, every linear HSL is representable as a sub HSL of a product of linear ones). In a linear HSL one may construct disjunction as ((x -> y) -> y) ^ ((y -> x) -> x) The factoid of interest is this sort-of converse: the only HSL varieties in which every member is a lattice are varieties of linear HSLs.