Weak omega-categories from intensional type theory

DOI10.2168/LMCS-6(3:24)2010zbMath1250.03127arXiv0812.0409OpenAlexW2951884685MaRDI QIDQ2786141

Peter LeFanu Lumsdaine

Publication date: 21 September 2010

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

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

zbMATH Keywords

operadsidentity typesintuitionistic type theorydependent type theory\(n\)-categorieshigher categoriesinfinity-categoriesomega-categoriesintensional type theoryunivalent foundations

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Metamathematics of constructive systems (03F50)

Related Items (15)

Naive cubical type theory ⋮ Hom weak ω-categories of a weak ω-category ⋮ Homotopy type theory and Voevodsky’s univalent foundations ⋮ Martin-Löf complexes ⋮ Unnamed Item ⋮ Observability in the univalent universe ⋮ Bicategorical type theory: semantics and syntax ⋮ A categorical characterization of strong Steiner \(\omega\)-categories ⋮ Unnamed Item ⋮ A type theory for synthetic $\infty$-categories ⋮ Mathesis Universalis and Homotopy Type Theory ⋮ Homotopy-Theoretic Models of Type Theory ⋮ Univalence in locally Cartesian closed categories ⋮ Unnamed Item ⋮ A homotopy-theoretic model of function extensionality in the effective topos

This page was built for publication: Weak omega-categories from intensional type theory