Phil Scott has been teaching me about the lambda calculus and related stuff. He noted that in getting a cartesian closed category from intuitionistic logic,
At the risk of boring people by repeating a point I've made on this list before: 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? Ccc's without coproducts (e.g. domains and continuous maps) arise in the study of call-by-name languages with effects (e.g. divergence). But they are not models of intuitionistic logic. I appreciate that all John said was that a model constructed from syntax is a ccc, which is true because it's a bi-ccc, so he didn't actually contradict this point. Paul