Abstract
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 \((\infty , 1)\)-categories with finite limits.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
Notes
However, fibrations are not necessarily closed under retracts.
This ensures that the \(\Sigma \)-type is given by composition and hence preserved by morphisms of categorical models of type theory, cf. Definition 9.6.
References
Avigad, J., Kapulkin, K., Lumsdaine, P.L.: Homotopy limits in type theory. Math. Struct. Comput. Sci. 25(5), 1040–1070 (2015)
Baues, H.J.: Algebraic Homotopy, Cambridge Studies in Advanced Mathematics, vol. 15. Cambridge University Press, Cambridge (1989)
Brown, K.S.: Abstract homotopy theory and generalized sheaf cohomology. Trans. Am. Math. Soc. 186, 419–458 (1973)
Cisinski, D.-C.: Catégories dérivables. Bull. Soc. Math. Fr. 138(3), 317–393 (2010)
Cisinski, D.-C.: Invariance de la \(K\)-théorie par équivalences dérivées. J. K-Theory 6(3), 505–546 (2010)
Dwyer, W.G., Kan, D.M.: Calculating simplicial localizations. J. Pure Appl. Algebra 18(1), 17–35 (1980)
Favonia, K.-B. Hou, Finster, E., Licata, D.R., Lumsdaine, P.L.: A mechanization of the Blakers–Massey connectivity theorem in homotopy type theory, Proceedings of the 31st annual ACM/IEEE symposium on logic in computer science, pp. 565–574 (2016)
Gambino, N., Garner, R.: The identity type weak factorisation system. Theor. Comput. Sci. 409(1), 94–109 (2008)
Garner, R.: Two-dimensional models of type theory. Math. Struct. Comput. Sci. 19(4), 687–736 (2009)
Hirschhorn, P.S.: Model Categories and Their Localizations, Mathematical Surveys and Monographs, vol. 99. American Mathematical Society, Providence (2003)
Bauer, A., Gross, J., Lumsdaine, P. LeFanu, Shulman, M.: The HoTT Library. https://github.com/HoTT/HoTT. open code repository. Accessed 31 Jan 2019
Hovey, M.: Model Categories, Mathematical Surveys and Monographs, vol. 63. American Mathematical Society, Providence (1999)
Jacobs, B.: Comprehension categories and the semantics of type dependency. Theor. Comput. Sci. 107(2), 169–207 (1993)
Jacobs, B.: Categorical Logic and Type Theory, Studies in Logic and the Foundations of Mathematics, vol. 141. North-Holland Publishing Co., Amsterdam (1999)
Joyal, A.: The theory of quasi-categories and its applications, Quadern 45, Vol. II. Centre de Recerca Matem‘atica, Barcelona (2008)
Joyal, A.: Notes on clans and tribes (2017). arXiv:1710.10238. Accessed 31 Jan 2019
Kan, D.M.: On c. s. s. complexes. Am. J. Math. 79, 449–476 (1957)
Kapulkin, K.: Locally cartesian closed quasi-categories from type theory. J. Topol. 10(4), 1029–1049 (2017)
Kapulkin, K., Lumsdaine, P.L.: The homotopy theory of type theories. Adv. Math. 337, 1–38 (2018)
Kapulkin, K., Szumiło, K.: Quasicategories of frames of cofibration categories. Appl. Categ. Struct. 25(3), 323–347 (2017)
Latch, D.M., Thomason, R.W., Wilson, W.S.: Simplicial sets from categories. Math. Z. 164(3), 195–214 (1979)
Lumsdaine, P.L., Warren, M.A.: The local universes model: an overlooked coherence construction for dependent type theories, ACM Trans. Comput. Log. 16(3), Art. 23, 31 (2015)
Lurie, J.: Higher Topos Theory, Annals of Mathematics Studies, vol. 170. Princeton University Press, Princeton (2009)
Munson, B.A., Volić, I.: Cubical Homotopy Theory, New Mathematical Monographs, vol. 25. Cambridge University Press, Cambridge (2015)
Nikolaus, T., Schreiber, U., Stevenson, D.: Principal \(\infty \)-bundles: presentations. J. Homotopy Relat. Struct. 10(3), 565–622 (2015)
Quillen, D.: Higher algebraic \(K\)-theory. I, Algebraic \(K\)-theory, I: Higher \(K\)-theories (Proc. Conf., Battelle Memorial Inst., Seattle, Wash., 1972), Lecture Notes in Math., Vol. 341, pp. 85–147. Springer, Berlin (1973)
Rasekh, N.: A theory of elementary higher toposes (2018). arXiv:1805.03805
Rădulescu-Banu, A.: Cofibrations in homotopy theory (2006). arXiv:math/0610009v4
Rourke, C.P., Sanderson, B.J.: \(\Delta \)-sets. I. homotopy theory. Quart. J. Math. Oxford Ser. 22, 321–338 (1971)
Schwede, S.: The \(p\)-order of topological triangulated categories. J. Topol. 6(4), 868–914 (2013)
Shulman, M.: Univalence for inverse diagrams and homotopy canonicity. Math. Struct. Comput. Sci. 25(5), 1203–1277 (2015)
Szumiło, K.: Homotopy theory of cofibration categories. Homol. Homot. Appl. 18(2), 345–357 (2016)
Szumiło, K.: Frames in cofibration categories. J. Homot. Relat. Struct. 12(3), 577–616 (2017)
Szumiło, K.: Homotopy theory of cocomplete quasicategories. Algebra Geom. Topol. 17(2), 765–791 (2017)
The Univalent Foundations, Homotopy type theory—univalent foundations of mathematics, The Univalent Foundations Program, Princeton, NJ; Institute for Advanced Study (IAS), Princeton NJ (2013)
van den Berg, B., Garner, R.: Types are weak \(\omega \)-groupoids. Proc. Lond. Math. Soc. 102(2), 370–394 (2011)
Voevodsky, V., Ahrens, B., Grayson, D. et al.: UniMath: Univalent Mathematics. https://github.com/UniMath
Waldhausen, F.: Algebraic \(K\)-theory of spaces, Algebraic and geometric topology (New Brunswick, N.J., 1983), Lecture Notes in Math., vol. 1126, pp. 318–419. Springer, Berlin (1985)
Acknowledgements
This work would not have been possible without the support and encouragement of André Joyal. We are also very grateful to him for sharing an early draft of his manuscript on the theory of tribes with us.
Author information
Authors and Affiliations
Corresponding author
Additional information
Publisher's Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
Rights and permissions
About this article
Cite this article
Kapulkin, K., Szumiło, K. Internal languages of finitely complete \((\infty , 1)\)-categories. Sel. Math. New Ser. 25, 33 (2019). https://doi.org/10.1007/s00029-019-0480-0
Published:
DOI: https://doi.org/10.1007/s00029-019-0480-0