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