Internal languages of finitely complete \((\infty , 1)\)-categories

DOI10.1007/s00029-019-0480-0zbMath1462.18007arXiv1709.09519OpenAlexW2962703185MaRDI QIDQ2414596

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)

Related Items (4)

Homotopy groups of cubical sets ⋮ A general framework for the semantics of type theory ⋮ Indexed type theories ⋮ Univalence and completeness of Segal objects

Uses Software

• UniMath
• HoTT
• GitHub

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Principal \(\infty\)-bundles: presentations
• Homotopy theory of cofibration categories
• Homotopy theory of cocomplete quasicategories
• The identity type weak factorisation system
• Calculating simplicial localizations
• Comprehension categories and the semantics of type dependency
• Simplicial sets from categories
• Categorical logic and type theory
• The homotopy theory of type theories
• Quasicategories of frames of cofibration categories
• Frames in cofibration categories
• The Local Universes Model
• Catégories dérivables
• Types are weak ω -groupoids
• Invariance de laK-Théorie par équivalences dérivées
• Locally cartesian closed quasi‐categories from type theory
• On c.s.s. Complexes
• Two-dimensional models of type theory
• Higher algebraic K-theory: I
• A Mechanization of the Blakers-Massey Connectivity Theorem in Homotopy Type Theory
• The n -order of algebraic triangulated categories
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Higher Topos Theory (AM-170)
• Δ-SETS I: HOMOTOPY THEORY
• Abstract homotopy theory and generalized sheaf cohomology
• Homotopy limits in type theory
• Univalence for inverse diagrams and homotopy canonicity

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