-Limits and colimits
limits and colimits
limit and colimit
limits and colimits by example
commutativity of limits and colimits
connected limit, wide pullback
preserved limit, reflected limit, created limit
product, fiber product, base change, coproduct, pullback, pushout, cobase change, equalizer, coequalizer, join, meet, terminal object, initial object, direct product, direct sum
end and coend
Equality and Equivalence
equality (definitional?, propositional, computational, judgemental, extensional, intensional, decidable)
identity type, equivalence in homotopy type theory
isomorphism, weak equivalence, homotopy equivalence, weak homotopy equivalence, equivalence in an (∞,1)-category
natural equivalence, natural isomorphism
principle of equivalence
fiber product, pullback
linear equation, differential equation, ordinary differential equation, critical locus
Euler-Lagrange equation, Einstein equation, wave equation
Schrödinger equation, Knizhnik-Zamolodchikov equation, Maurer-Cartan equation, quantum master equation, Euler-Arnold equation, Fuchsian equation, Fokker-Planck equation, Lax equation
Paths and cylinders
Model category theory
Producing new model structures
Presentation of -categories
for stable/spectrum objects
for stable -categories
for -sheaves / -stacks
A homotopy pullback is a special kind of homotopy limit: the appropriate notion of pullback in the context of homotopy theory. Homotopy pullbacks model the quasi-category pullbacks in the (infinity,1)-category that is presented by a given homotopical category. Since pullbacks are also called fiber products, homotopy pullbacks are also called homotopy fiber products.
A homotopy pushout is the dual concept.
For more details see homotopy limit.
In the context of homotopy type theory a homotopy pullback is the interpretation of the space of solutions to an equation.
In category theory
As with all homotopy limits, there is both a local and a global notion of homotopy pullback.
The global definition says that the homotopy pullback of a cospan in a category with weak equivalences is its image under the right derived functor of the base change functor .
The local definition says that the homotopy pullback of in a category with a notion of homotopy consists of a square
that commutes up to homotopy, and such that for any other square
that commutes up to homotopy, there exists a morphism , unique up to homotopy, making the two triangles commute up to homotopy, and similarly for homotopies and higher homotopies. In other words, there is an equivalence
between the space of maps and the space of homotopy commutative squares with vertex .
In good situations, such as when are fibrant in a model category, the two constructions agree up to weak equivalence.
Note that in both cases, there is a canonical map from the actual pullback to the homotopy pullback . In the global case this comes by the definition of a derived functor; in the local case it comes because a commutative square is, in particular, a homotopy commutative one.
In homotopy type theory
In homotopy type theory the homotopy pullback of a term of function type
along a term of function type
is given formally by precisely the same formula that would also define the ordinary fiber product of functions of sets, namely by
Spelled out, this is the dependent sum over the dependent identity type over the evaluation of and .
What in classical logic is interpreted as the set of pairs such that and are equal here becomes the restriction of a mapping cocylinder.
Formal proof that this is the homotopy pullback in homotopy type theory is in (Brunerie). Proof in the categorical semantics of homotopy type theory is below.
We discuss various concrete constructions by ordinary pullbacks and ordinary limits such that under some sufficient conditions these compute homotopy pullbacks, up to weak equivalence.
Let be a diagram in some model category. Then sufficient conditions for the ordinary (1-categorical) pullback to present the homotopy pullback of the diagram are
Both statements are classical. They are reviewed for instance as Lurie, prop. A.2.4.4. The proof of the second statement is spelled out here.
Due to prop. 1 one typically computes homotopy pullbacks of a diagram by first forming a resolution of one of the two morphisms by a fibration and then forming an ordinary pullback.
If all objects involved are already fibrant, then such a resolution is provided by the factorization lemma. This says that a fibrant resoltuion of is given by the total composite vertical morphism in
where is a path object for the fibrant object (For instance, when is a closed monoidal homotopical category then this can be taken to be the internal hom with an interval object .)
Then by prop. 1 we have
If in all three objects are fibrant objects, then the homotopy pullback of this diagram is presented by the ordinary limit in
or, which is the same up to isomorphism, as the ordinary pullback
The canonical morphism here is induced by the canonical section into the path space object, hence by the commutativity of the diagram
The homotopy pullback constructed in this way is an example of a strict homotopy limit, as mentioned at homotopy limit. In such a case, one can say that an arbitrary homotopy-commutative square
is a homotopy pullback square if the induced morphism from to the strict homotopy pullback is a weak equivalence.
A useful class of example of this is implied by the following:
The global projective model structure on simplicial presheaves is right proper. So by prop. 1 the ordinary pullback in question presents the homotopy pullback in the global structure. By the discussion at homotopy limit and Bousfield localization of model categories, this presents the (∞,1)-pullback of the diagram of (∞,1)-presheaves, and the fibrant replacement of that pullback in the local model structure presents the (∞,1)-sheafification of this (∞,1)-presheaf. This is (essentially by definition, see (∞,1)-topos) a left exact (∞,1)-functor and hence preserves finite (∞,1)-limits.
In homotopy type theory
If we unwind the categorical semantics of the above definition
of the homotopy pullback in homotopy type theory, we re-obtain the above prescription for how to construct homotopy pullbacks.
So let the ambient category be a suitable type-theoretic model category.
The type is obtained by substitution from the identity type of . By the discussion there, the categorical semantics of substitution is given by pullback of the fibrations that interpret the dependent types, and so this is interpreted as the pullback of the path space object of :
Forming the dependent sum over is simply interpreted as regarding the resulting object as an object in instead of as an object in the slice category .
Since by assumption on the categorical interpretation of a type, all objects here are fibrant, this coincides with the expression of the homotopy pullback from corollary 1 above.
Specifically, let be a function, then the categorical semantics for the expression
is the canonical fibration replacement of as it appears notably in the factorization lemma
Homotopy fiber characterization
In plain homotopy types:
is a homotopy pullback diagram precisely if it induces a weak equivalence on all homotopy fibers
e.g. (CPS, 5.2)
Of particular interest are consecutive homotopy pullbacks of point inclusions. These give rise to fiber sequences and loop space objects.
See the references at homotopy limit .
A fairly comprehensive resource is the appendix of
In terms of homotopy type theory
A proposal for a formalization of homotopy pushouts by higher inductive types in homotopy type theory has been given in
A HoTT-Coq-coding of homotopy pullbacks and pushouts is in