# Definition of $(\infty,1)$-category in HoTT [duplicate]

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.

## marked as duplicate by Noah Snyder, Mike Shulman ct.category-theory StackExchange.ready(function() { if (StackExchange.options.isMobile) return; $('.dupe-hammer-message-hover:not(.hover-bound)').each(function() { var$hover = $(this).addClass('hover-bound'),$msg = $hover.siblings('.dupe-hammer-message');$hover.hover( function() { $hover.showInfoMessage('', { messageElement:$msg.clone().show(), transient: false, position: { my: 'bottom left', at: 'top center', offsetTop: -7 }, dismissable: false, relativeToBody: true }); }, function() { StackExchange.helpers.removeMessages(); } ); }); }); Jul 5 '18 at 4:09

• 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? – ReadTooMuch Jul 5 '18 at 9:07
• 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. – Noah Snyder Jul 5 '18 at 15:07

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.
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.