2017/09/27 by Kapulkin, Chris, Szumiło, Karol
#03B15 (primary) #18G55 #55U35 #Algebraic Topology (math.AT) #Category Theory (math.CT) #FOS: Mathematics #Logic (math.LO)
paper · doi:10.48550/arxiv.1709.09519
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.