Internal languages of finitely complete ( , 1)-categories

DOI10.1007/S00029-019-0480-0MaRDI QIDQ2414596zbMATH OpenOpenAlexFDO

Authors Krzysztof Kapulkin, Karol Szumiło

Publication date 17 May 2019

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

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

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)

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.

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

Cites work

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

Cited in

(8)

• Homotopy type theory as internal languages of diagrams of \(\infty\)-logoses
• Homotopy groups of cubical sets
• A general framework for the semantics of type theory
• Indexed type theories
• Univalence and completeness of Segal objects
• Univalence for inverse EI diagrams
• A type theory for synthetic \(\infty\)-categories
• scientific article; zbMATH DE number 4057495 (Why is no real title available?)

Describes a project that uses

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)