The identity type weak factorisation system
From MaRDI portal
Publication:959823
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
Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items
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
