A type theory for synthetic $\infty$-categories

zbMath1437.18016arXiv1705.07442MaRDI QIDQ3121017

Michael Shulman, Emily Riehl

Publication date: 19 March 2019

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

zbMATH Keywords

homotopy type theory\(\infty\)-categoriesSegal spacesRezk spaces

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Abstract and axiomatic homotopy theory in algebraic topology (55U35) Homotopical algebra, Quillen model categories, derivators (18N40) 2-categories, bicategories, double categories (18N10) Type theory (03B38) ((infty,1))-categories (quasi-categories, Segal spaces, etc.); (infty)-topoi, stable (infty)-categories (18N60)

Related Items (19)

Unnamed Item ⋮ Higher Structures in Homotopy Type Theory ⋮ A formal logic for formal category theory ⋮ Two-level type theory and applications ⋮ Bicategorical type theory: semantics and syntax ⋮ Canonicity and homotopy canonicity for cubical type theory ⋮ Yoneda lemma for simplicial spaces ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ On the topological characterization of gestures in a convenient category of spaces ⋮ Indexed type theories ⋮ Unnamed Item ⋮ Filter quotients and non-presentable \((\infty,1)\)-toposes ⋮ Cubical Agda: A dependently typed programming language with univalence and higher inductive types ⋮ Syntax and models of Cartesian cubical type theory

Uses Software

• cubicaltt

Cites Work

• Fibrations and Yoneda's lemma in an \(\infty\)-cosmos
• Homotopy coherent adjunctions and the formal theory of monads
• A Cartesian presentation of weak \(n\)-categories
• Sheaves in geometry and logic: a first introduction to topos theory
• Categorical logic and type theory
• Quasi-categories and Kan complexes
• Reedy categories and the \(\varTheta\)-construction
• The simplicial model of univalent foundations (after Voevodsky)
• Yoneda lemma for complete Segal spaces
• Weak omega-categories from intensional type theory
• The Local Universes Model
• Types are weak ω -groupoids
• On a Topological Topos
• A model for the homotopy theory of homotopy theory
• Cubical Type Theory: a constructive interpretation of the univalence axiom
• Brouwer's fixed-point theorem in real-cohesive homotopy type theory
• Fibrations of $\infty$-categories
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Higher Topos Theory (AM-170)
• 2-Dimensional Directed Type Theory
• Univalent categories and the Rezk completion
• The univalence axiom for elegant Reedy presheaves
• Yoneda lemma for simplicial spaces
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: A type theory for synthetic $\infty$-categories