Re: Voevodsky on the homotopy lambda calculus

[Andrej Bauer <Andrej.Bauer@andrej.com>]

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