A wild category is a 1-dimensional approximation of an infinity-category that is definable in Book HoTT. It consists of
A type of objects
For objects a type of morphisms
For each object an identity
For objects a composition function
For objects and a morphism , equalities
For objects and morphisms and and , an equality .
If each is a set, then a wild category reduces to a precategory, but in general this condition is not imposed. This means that, for instance, there is a nontrivial pentagon identity for the associativities that does not necessarily commute, and so on. However, even lacking these coherence data, a wild category is sufficient for some purposes.
For example, we can define an initial object in a wild category to be an object such that is contractible for all . In cases when the wild category “is” actually a coherent higher category, this still gives the right answer, and it is sufficient for applications such as producing induction principles for higher inductive types. See the references for more specific examples.
References
Paolo Capriotti, Nicolai Kraus, Univalent Higher Categories via Complete Semi-Segal Types, arxiv, 2017
Nicolai Kraus, Jakob von Raumer, Path Spaces of Higher Inductive Types in Homotopy Type Theory, arxiv, 2019
Mike Shulman, Impredicative Encodings, Part 3, blog post, 2018
Revision on June 7, 2022 at 22:35:02 by
Anonymous?.
See the history of this page for a list of all contributions to it.