Internal Languages of Finitely Complete $(\infty, 1)$-categories
Category Theory
2019-04-05 v2 Algebraic Topology
Logic
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\"of Type Theory with dependent sums and intensional identity types is the internal language of -categories with finite limits.
Cite
@article{arxiv.1709.09519,
title = {Internal Languages of Finitely Complete $(\infty, 1)$-categories},
author = {Chris Kapulkin and Karol Szumiło},
journal= {arXiv preprint arXiv:1709.09519},
year = {2019}
}
Comments
41 pages, minor revisions