Weak ω-Categories from Intensional Type Theory

DOI10.1007/978-3-642-02273-9_14zbMath1200.03050OpenAlexW2018415539MaRDI QIDQ3637194

Peter LeFanu Lumsdaine

Publication date: 7 July 2009

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-02273-9_14

Mathematics Subject Classification ID

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

Related Items (10)

Canonicity of weak \(\omega\)-groupoid laws using parametricity theory ⋮ The construction of set-truncated higher inductive types ⋮ Homotopical patch theory ⋮ Meaning explanations at higher dimension ⋮ Monoidal weak ω-categories as models of a type theory ⋮ On the ∞$\infty$‐topos semantics of homotopy type theory ⋮ 2-Dimensional Directed Type Theory ⋮ Homotopy limits in type theory ⋮ Type Theory and Homotopy ⋮ A rewriting coherence theorem with applications in homotopy type theory

Cites Work

• Unnamed Item
• Unnamed Item
• The identity type weak factorisation system
• Generalized algebraic theories and contextual categories
• Monoidal globular categories as a natural environment for the theory of weak \(n\)-categories
• Categorical logic and type theory
• The petit topos of globular sets
• \(\Lambda\)-cofibration categories and the homotopy categories of global actions and simplicial complexes
• Types are weak ω -groupoids
• Homotopy theoretic models of identity types

This page was built for publication: Weak ω-Categories from Intensional Type Theory