Voevodsky on the homotopy lambda calculus

Voevodsky on the homotopy lambda calculus

[John Baez]

As has already been pointed out here, Vladimir Voevodsky is giving
lectures at Stanford on the "homotopy lambda calculus":

http://math.stanford.edu/distinguished_voevodsky.htm

Can anyone report on what he said?

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, one takes sequents

Gamma |- Delta

as objects and *equivalence classes* of proofs as morphisms.
One needs to take equivalence classes to get composition of
morphisms to be associative, etc.  From an n-categorical
viewpoint it's natural to avoid working with equivalence classes
and instead use 2-morphisms between morphisms, like associators,
and so on, thus getting a "weak cartesian closed omega-category" -
a concept which, alas, has probably not been defined yet.

For someone like Voevodsky it would be natural to use ideas from
homotopy theory instead and define something like a "cartesian
closed category up to coherent homotopy".  Such a thing should
be lurking in the ordinary typed lambda calculus.

Is this what Voevodsky is talking about?  Or...?

Best,
jb

Re: Voevodsky on the homotopy lambda calculus

[Andrej Bauer]

On Wednesday 22 February 2006 22:53, John Baez wrote:
> From an n-categorical
> viewpoint it's natural to avoid working with equivalence classes
> and instead use 2-morphisms between morphisms, like associators,
> and so on, thus getting a "weak cartesian closed omega-category" -
> a concept which, alas, has probably not been defined yet.

I don't know about the omega-wheel, but at least the 2-wheel needs not be
reinvented. For "cartesian closed 2-categories", a relevant reference is

  R.A.G. Seely, "Modelling computations: A 2-categorical framework". In
  Proceedings of the Second Symposium on Logic in Computer Science, pages
  61--71, IEEE Computer Science Press, June 1987.

I believe the above paper is "the first" on this topic (am I wrong?), and
there must be more recent work. I know Neil Ghani did some, but Google also
knows about "2-Lambda Calculus" by David Rydeheard, see
http://www.cs.man.ac.uk/~david/publications/TwoLambdaCalculus.ps .

Andrej

Re: Voevodsky on the homotopy lambda calculus

[Paul B Levy]

> 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