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