Topological and Simplicial Models of Identity Types

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

zbMATH Keywords

homotopy theorycategorical semanticsidentity typesdependent type theory

Mathematics Subject Classification ID

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