Re: Voevodsky on the homotopy lambda calculus

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

> 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