Internal languages of finitely complete ( , 1)-categories

DOI10.1007/S00029-019-0480-0zbMATH Open1462.18007arXiv1709.09519OpenAlexW2962703185MaRDI QIDQ2414596FDOQ2414596

Authors: Krzysztof Kapulkin, Karol Szumiło 

Publication date: 17 May 2019

Published in: Selecta Mathematica. New Series (Search for Journal in Brave)

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 $(infty,1)$-categories with finite limits.

Full work available at URL: https://arxiv.org/abs/1709.09519

Recommendations

• A type theory for synthetic \(\infty\)-categories
• Fibred fibration categories
• Univalence for inverse diagrams and homotopy canonicity
• The Homotopy Theory of (∞,1)-Categories
• Extending homotopy type theory with strict equality
• Higher groups in homotopy type theory
• Univalence for inverse EI diagrams
• Fibrations and Yoneda's lemma in an \(\infty\)-cosmos
• Higher categories and homotopical algebra
• Natural models of homotopy type theory

zbMATH Keywords

homotopy type theory\((\infty,1)\)-categories

Mathematics Subject Classification ID

Abstract and axiomatic homotopy theory in algebraic topology (55U35) Type theory (03B38) ((infty,1))-categories (quasi-categories, Segal spaces, etc.); (infty)-topoi, stable (infty)-categories (18N60)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Categorical logic and type theory
• Catégories dérivables
• Higher algebraic K-theory: I
• Higher Topos Theory (AM-170)
• Title not available (Why is that?)
• Types are weak \(\omega \)-groupoids
• Homotopy type theory. Univalent foundations of mathematics
• The identity type weak factorisation system
• Title not available (Why is that?)
• Principal \(\infty\)-bundles: presentations
• Comprehension categories and the semantics of type dependency
• Abstract homotopy theory and generalized sheaf cohomology
• Δ-SETS I: HOMOTOPY THEORY
• Calculating simplicial localizations
• Two-dimensional models of type theory
• Invariance of the \(K\)-theory for derived equivalences
• Homotopy theory of cofibration categories
• On c.s.s. Complexes
• Quasicategories of frames of cofibration categories
• The n -order of algebraic triangulated categories
• Homotopy theory of cocomplete quasicategories
• The local universes model: an overlooked coherence construction for dependent type theories
• Univalence for inverse diagrams and homotopy canonicity
• Simplicial sets from categories
• The homotopy theory of type theories
• Homotopy limits in type theory
• Frames in cofibration categories
• Locally Cartesian closed quasi-categories from type theory
• A mechanization of the Blakers-Massey connectivity theorem in homotopy type theory

Cited In (7)

• Homotopy groups of cubical sets
• A general framework for the semantics of type theory
• Title not available (Why is that?)
• Univalence and completeness of Segal objects
• Indexed type theories
• Univalence for inverse EI diagrams
• A type theory for synthetic \(\infty\)-categories

Uses Software

• UniMath
• HoTT
• GitHub

This page was built for publication: Internal languages of finitely complete \((\infty , 1)\)-categories

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2414596)