Axioms and Models for Concrete Homotopy
Résumé
By concrete homotopy we mean homotopy based on a path functor, as in the original model found in the category of k-spaces. The point of the axiomatics is not that there are many models (right now we know of only three, which we will call here a, b and c ) but that the construction of the higher homotopy structure of an object in such a model is extremely simple and that models b and c have remarkable properties. So to be a model a finitely complete category C is required to have - A class of maps F, the fibrations which obey standard properties: closure under pullback and composition, with projections and isos being fibrations. - A path endofunctor P with the usual two natural projections to the identity endofunctor and unit path inclusion from the identity, wich the requirement that PX →X×X is a fibration. The essential point is that this functor is fibered w.r.t. F and that the above map is a fibration. These suffice to define a homotopy between maps, and we need additional axioms to say that PX is a groupoid modulo homotopy and that any fibration is equipped with an action of it, with the usual equations holding modulo homotopy. Thus in model a fibrations are just Hurewicz fibrations and P is a suitably fibered version of the usual path functor. In general P is not required to have a left ("cylinder") adjoint, and it is not the case for models b, c. The fact that it is fibered allows an easy construction of the groupoid π1 for any fibration and since this groupoid is internal inside the world of fibrations, the π1 construction can be just iterated to give the higher homotopy structure. Thus the homotopy higher groupoid of X is not a set-groupoid, but something living in a suitable category of "covers" of X . Models c, d are based on small categories. First a path functor is defined in Cat, in which objects are zig-zags of maps, and morphisms suitably defined "bimodules". This construction is similar but distinct from the "Hammock" construction given by Dwyer-Kan. Its natural notion of concatenation of paths is unfortunately not functorial. We know of two ways to remedy this: - In b concatenation is tweaked, which makes the unit valid only up to homotopy. Fibrations there are a kind "generalized (cleft) Grothendieck bifibrations". - In c the natural--in an intuitive, not technical sense--order structure on P is quotiented out, which makes the fibrations ordinary (cleft) Grothendieck fibrations. Thus constructions b, c give a new approach to homotopy in Cat, much more concrete (and less technical) than the Quillen model structure defined by Thomason in 1980. In addition fibrations in model c are exponentiable, which allows the interpretation of dependent types and the lambda-calculus, with P obeying the necessary axioms to interpret the Martin-Löf identity predicate. This is being worked out by my student Robert Hein. Moreover this model has the counterintuitive property that path composition is strictly associative, with a strict unit. The first offshoot of this surprising result is a conjecture that generalizes the well-known theorem that for a category X the groupoid π1X is its universal associated groupoid: we formulate a conjecture that holds for any πn.