Re: intuitionism and disjunction

[Paul B Levy <P.B.Levy@cs.bham.ac.uk>]

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