Voevodsky on the homotopy lambda calculus

["John Baez" <baez@math.ucr.edu>]

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