5
$\begingroup$

Reading Lurie's Higher topos theory got me thinking, if we can think of $(\infty,1)-$categories as (1-)categories enriched over $\infty$-groupoid, then wouldn't the internal definition of an $(\infty,1)$-category in Homotopy type theory be the usual univalent category but with homs as usual types instead of sets?

This seems to correspond to the notion of category in the HoTT library although technically the HoTT book defines a category to have hom-sets instead of types.

The first higher category I can think of is $\infty$-groupoid where the type of objects is simply $\mathcal U_0$, and then morphisms are the types $X \to Y$ which I am assuming isn't truncated or anything. Then the circle $S^1$ defined as a higher inductive type is in this category. And the hom-type $S^1\to S^1$ is some sort of elimator of the HIT for $S^1$ which is itself a HIT.

This (I think) obviously only works if our ambient category is $\infty$-groupoid itself (which is some form of HoTT). I am not sure this applies to all $\infty$-toposes.

Improve this question
$\endgroup$
2
  • 1
    $\begingroup$ I am finding this being marked as a duplicate a bit lazy, the last question was from 5 years ago, surely something has at least changed? $\endgroup$
    – ReadTooMuch
    Jul 5, 2018 at 9:07
  • 2
    $\begingroup$ There have been a few recent answers and edits there which include what has changed in the intervening time. A follow-up question that’s different from the old one may well be appropriate. $\endgroup$
    – Noah Snyder
    Jul 5, 2018 at 15:07

1 Answer 1

Reset to default
5
$\begingroup$

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.

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.

Improve this answer
$\endgroup$
4
  • 1
    $\begingroup$ I don't know that it is universally believed that defining semisimplicial types is impossible; all we know is that no one has managed to do it yet, right? $\endgroup$
    – Mike Shulman
    Jul 5, 2018 at 4:07
  • 3
    $\begingroup$ More recent references than HTS are arxiv.org/abs/1705.03307 and arxiv.org/abs/1707.03693. $\endgroup$
    – Mike Shulman
    Jul 5, 2018 at 4:08
  • 1
    $\begingroup$ @MikeShulman Yes, but if no one can construct some mathematical object for long enough time, then it is usually conjectured that it is impossible to do so. Maybe I had the wrong impression that semisimplicial types fell under this category, but I didn't see many people expressing the belief that they are constructible. $\endgroup$
    – Valery Isaev
    Jul 5, 2018 at 4:22
  • 3
    $\begingroup$ Some people certainly believe it is impossible, but I don't think that belief is "universal". I don't think we've really been trying for very long, in the grand scheme of things, and not very many people are actively working on this problem either. And I haven't yet heard a convincing argument for why semisimplicial types would be impossible, when other "infinite structures" like globular types are possible. $\endgroup$
    – Mike Shulman
    Jul 5, 2018 at 20:24

Not the answer you're looking for? Browse other questions tagged or ask your own question.