Return to Answer

typo

Source Link

edited Aug 4, 2021 at 5:42

18.4k
3
85
175

We can't define $(\infty,1)$-categories in HoTT in this way since the enrichment must be strict. That is, the composition operation must be strictly associative and strictly unital. In HoTT, we can only require these properties to hold up to a homotopy. Then we also must add a coherence path between these homotopies (similar to the pentagon identity for monoidal categories) and then a coherence path between these coherence paths, and so on. It is commonly believed that it is impossible to describe an infinite amount of coherence data in plain HoTT. A simpler problem that involves such coherence issues is the problem of constructing simesemi-simplicial types, which is also believed to be impossible.

There are different extensions of HoTT that were suggested to solve this problem such as HTS which adds a type of "strict equalities" (compared to the type of paths in ordinary HoTT). There are also completely different approaches to the problem of defining $(\infty,1)$-categories in HoTT-style such as the one suggested in this paper.

We can't define $(\infty,1)$-categories in HoTT in this way since the enrichment must be strict. That is, the composition operation must be strictly associative and strictly unital. In HoTT, we can only require these properties to hold up to a homotopy. Then we also must add a coherence path between these homotopies (similar to the pentagon identity for monoidal categories) and then a coherence path between these coherence paths, and so on. It is commonly believed that it is impossible to describe an infinite amount of coherence data in plain HoTT. A simpler problem that involves such coherence issues is the problem of constructing sime-simplicial types, which is also believed to be impossible.

We can't define $(\infty,1)$-categories in HoTT in this way since the enrichment must be strict. That is, the composition operation must be strictly associative and strictly unital. In HoTT, we can only require these properties to hold up to a homotopy. Then we also must add a coherence path between these homotopies (similar to the pentagon identity for monoidal categories) and then a coherence path between these coherence paths, and so on. It is commonly believed that it is impossible to describe an infinite amount of coherence data in plain HoTT. A simpler problem that involves such coherence issues is the problem of constructing semi-simplicial types, which is also believed to be impossible.

Source Link

created Jul 4, 2018 at 18:57

Valery Isaev

4.5k
1
19
35

We can't define $(\infty,1)$-categories in HoTT in this way since the enrichment must be strict. That is, the composition operation must be strictly associative and strictly unital. In HoTT, we can only require these properties to hold up to a homotopy. Then we also must add a coherence path between these homotopies (similar to the pentagon identity for monoidal categories) and then a coherence path between these coherence paths, and so on. It is commonly believed that it is impossible to describe an infinite amount of coherence data in plain HoTT. A simpler problem that involves such coherence issues is the problem of constructing sime-simplicial types, which is also believed to be impossible.