Homotopy Type Theory
wild category (changes)

Showing changes from revision #1 to #2: Added | Removed | Changed

Wild categories

Definition

A wild category is a 1-dimensional approximation of an infinity-category that is definable in Book HoTT?. It consists of

  • A type obAob A of objects
  • For objects x,yx,y a type A(x,y)A(x,y) of morphisms
  • For each object xx an identity id x:A(x,x)id_x : A(x,x)
  • For objects x,y,zx,y,z a composition function :A(y,z)×A(x,y)A(x,z)\circ : A(y,z) \times A(x,y) \to A(x,z)
  • For objects x,yx,y and a morphism f:A(x,y)f:A(x,y), equalities fid x=f=id yff \circ id_x = f = id_y \circ f
  • For objects x,y,z,wx,y,z,w and morphisms f:A(x,y)f:A(x,y) and g:A(y,z)g:A(y,z) and h:A(z,w)h:A(z,w), an equality h(gf)=(hg)fh\circ (g\circ f) = (h\circ g)\circ f.

If each A(x,y)A(x,y) 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 00 such that A(0,x)A(0,x) is contractible for all xx. 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, Jakob von Raumer, Path Univalent Spaces of Higher Inductive Categories via Complete Semi-Segal Types in Homotopy Type Theory, arxiv, 2017

  • Mike Nicolai Shulman, Kraus, Jakob von Raumer, Impredicative Path Encodings, Spaces Part of 3 Higher Inductive Types in Homotopy Type Theory, blog arxiv post, 2019

  • Mike Shulman, Impredicative Encodings, Part 3, blog post, 2018

Last revised on February 10, 2019 at 18:18:04. See the history of this page for a list of all contributions to it.