Definition of $\left(\infty, 1\right)$-category in context of homotopy type theory

84 Views Asked by At

It has been proven that any locally presentable, locally cartesian closed $\left(\infty, 1\right)$-category models constructive dependent type theory (CDTT). From what I gather, this is supposed to generalize the fact that the category $\mathbf{sSet}$ of simplicial sets models CDTT.

But this confuses me. A common definition of an $\left(\infty, 1\right)$-category is a simplicial set for which every inner horn has a filler. In what sense, then, can $\mathbf{sSet}$ be considered an $\left(\infty, 1\right)$-category?

My confusion may just be terminological, but any clarification would be appreciated!