The identity type weak factorisation system

DOI10.1016/J.TCS.2008.08.030zbMath1157.68022arXiv0803.4349OpenAlexW2158324835WikidataQ61834707 ScholiaQ61834707MaRDI QIDQ959823

Richard Garner, Nicola Gambino

Publication date: 12 December 2008

Published in: Theoretical Computer Science (Search for Journal in Brave)

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

zbMATH Keywords

identity typedependent type theoryweak factorisation system

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (35)

Modeling Martin-Löf type theory in categories ⋮ A characterisation of elementary fibrations ⋮ Towards a directed homotopy type theory ⋮ Homotopical patch theory ⋮ Homotopy type theory and Voevodsky’s univalent foundations ⋮ Martin-Löf complexes ⋮ Combinatorial realizability models of type theory ⋮ Internal languages of finitely complete \((\infty , 1)\)-categories ⋮ Algebraic weak factorisation systems. I: Accessible AWFS. ⋮ Meaning explanations at higher dimension ⋮ The Local Universes Model ⋮ Identity types and weak factorization systems in Cauchy complete categories ⋮ Martin-Löf identity types in C-systems ⋮ On the ∞$\infty$‐topos semantics of homotopy type theory ⋮ Towards a constructive simplicial model of Univalent Foundations ⋮ Homotopical inverse diagrams in categories with attributes ⋮ Mathesis Universalis and Homotopy Type Theory ⋮ Homotopy-Theoretic Models of Type Theory ⋮ Exact completion of path categories and algebraic set theory. I: Exact completion of path categories ⋮ Univalence in locally Cartesian closed categories ⋮ Revisiting the categorical interpretation of dependent type theory ⋮ 2-Dimensional Directed Type Theory ⋮ Introduction – from type theory and homotopy theory to univalent foundations ⋮ Homotopy limits in type theory ⋮ A notion of homotopy for the effective topos ⋮ Univalence for inverse diagrams and homotopy canonicity ⋮ The Frobenius condition, right properness, and uniform fibrations ⋮ The simplicial model of univalent foundations (after Voevodsky) ⋮ A cubical model of homotopy type theory ⋮ Weak ω-Categories from Intensional Type Theory ⋮ Two-dimensional models of type theory ⋮ Type Theory and Homotopy ⋮ Natural models of homotopy type theory ⋮ Model structure on the universe of all types in interval type theory ⋮ MODELS OF MARTIN-LÖF TYPE THEORY FROM ALGEBRAIC WEAK FACTORISATION SYSTEMS

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Telescopic mappings in typed lambda calculus
• Homotopy-theoretic aspects of 2-monads
• Generalized algebraic theories and contextual categories
• Two-dimensional monad theory
• Constructions of factorization systems in categories
• Categorical logic and type theory
• Lax factorization algebras
• Locally cartesian closed categories and type theory
• Modular correspondence between dependent type theories and categories including pretopoi and topoi
• Homotopy theoretic models of identity types
• Strong stacks and classifying spaces
• Fibrations and geometric realizations
• Internal type theory
• FUNCTORIAL SEMANTICS OF ALGEBRAIC THEORIES

This page was built for publication: The identity type weak factorisation system