Dear Peter.
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
Can you explain the "of course" here, please? What were these reasons, and do they still hold water? I would have thought that tuples pose less of an ontological difficulty than functions.
there's this reason: if by a *bi*cartesian closed category one were to mean a ccc category whose dual is also ccc
What I meant was cartesian closed category with finite coproducts.
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.
I don't know what you mean - maybe that product types are more similar to function types than sum types are? If so, I agree, but I was comparing function types with sum types, not (function and sum) with (function and product). Paul