Topological and Simplicial Models of Identity Types
From MaRDI portal
Publication:2946651
DOI10.1145/2071368.2071371zbMath1352.03012arXiv1007.4638OpenAlexW1997582403MaRDI QIDQ2946651
Richard Garner, Benno van den Berg
Publication date: 17 September 2015
Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1007.4638
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (24)
Categorical structures for type theory in univalent foundations ⋮ Modeling Martin-Löf type theory in categories ⋮ A characterisation of elementary fibrations ⋮ A Hurewicz Model Structure for Directed Topology ⋮ Elementary fibrations of enriched groupoids ⋮ The Local Universes Model ⋮ Identity types and weak factorization systems in Cauchy complete categories ⋮ Martin-Löf identity types in C-systems ⋮ Towards a constructive simplicial model of Univalent Foundations ⋮ On the construction of functorial factorizations for model categories ⋮ Unnamed Item ⋮ Mathesis Universalis and Homotopy Type Theory ⋮ Homotopy-Theoretic Models of Type Theory ⋮ Unnamed Item ⋮ The Frobenius condition, right properness, and uniform fibrations ⋮ A cubical model of homotopy type theory ⋮ Unnamed Item ⋮ Equipping weak equivalences with algebraic structure ⋮ Unnamed Item ⋮ Models of Type Theory Based on Moore Paths ⋮ A homotopy-theoretic model of function extensionality in the effective topos ⋮ Type Theory and Homotopy ⋮ Natural models of homotopy type theory ⋮ MODELS OF MARTIN-LÖF TYPE THEORY FROM ALGEBRAIC WEAK FACTORISATION SYSTEMS
This page was built for publication: Topological and Simplicial Models of Identity Types
