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...?