Internal languages of finitely complete (\infty , 1)-categories
- Autores: Krzysztof Kapulkin, Karol Szumiło
- Localización: Selecta Mathematica, New Series, ISSN 1022-1824, Vol. 25, Nº. 2, 2019
- Idioma: inglés
- DOI: 10.1007/s00029-019-0480-0
- Enlaces
-
Resumen
We prove that the homotopy theory of Joyal’s tribes is equivalent to that of fibration categories. As a consequence, we deduce a variant of the conjecture asserting that Martin-Löf Type Theory with dependent sums and intensional identity types is the internal language of (∞,1) -categories with finite limits.
¿Es nuevo? Regístrese
Ventajas de registrarse
