nLab category with path objects

This is about the notion of path category in model category theory and homotopy theory. For the notion of path category in ordinary category theory, see path category.

---

Definition

A category with path objects or a path category is a category $\mathcal{C}$ equipped with two classes of morphisms called weak equivalences and fibrations, such that:

1. Fibrations are closed under composition

2. The pullback of a fibration along any other map exists and is again a fibration.

3. The pullback of an acyclic fibration along any other map is again an acyclic fibration.

4. Weak equivalences satisfy the two-out-of-six property: if $f:A \to B$, $g:B \to C$, $h:C \to D$ are three composable maps and both $g \circ f$ and $h \circ g$ are weak equivalences, then so are $f$, $g$, $h$ and $h \circ g \circ f$.

5. Isomorphisms are acyclic fibrations and every acyclic fibration has a section.

6. For any object $B$ there is a path space object $P B$ (not necessarily functorial in $B$).

7. $\mathcal{C}$ has a terminal object $1$ and every map $X \to 1$ to the terminal object is a fibration.

 Examples

• The syntactic category associated to a dependent type theory with identity types is a category with path objects.

• Given a Quillen model category $\mathcal{C}$ in which every object is cofibrant, the full subcategory of fibrant objects in $\mathcal{C}$ is a category with path objects.

• The category of topological spaces is a category with path objects where the homotopy equivalences are the weak equivalences and the Hurewicz fibrations are the the fibrations.

• A finitely complete category is a category with path objects in which every morphism is a fibration and only the isomorphisms are weak equivalences.

See also

• category of fibrant objects

• homotopy exact completion

References

• Benno van den Berg, Ieke Moerdijk, Exact completion of path categories and algebraic set theory: Part I: Exact completion of path categories, Journal of Pure and Applied Algebra 222 10 (2018) 3137-3181 [doi:10.1016/j.jpaa.2017.11.017, arXiv:1603.02456]

• Benno van den Berg, Martijn den Besten, Quadratic type checking for objective type theory (arXiv:2102.00905)