Topological and Simplicial Models of Identity Types

racting these leads us to introduce the notion of a path object category. This is a relatively simple axiomatic framework, which is nonetheless sufficiently strong to allow the construction of homotopy-theoretic models. Now by exhibiting suitable path object structures on Top and SSet, we endow those categories with the structure of a homotopy-theoretic model: and, in this way, obtain the desired topological and simplicial models of identity types. Categories and Subject Descriptors: F.4.1 [Mathematical Logic and Formal Languages]: Mathematical Logic—Lambda calculus and related systems General Terms: Theory Additional Key Words and Phrases: Dependent type theory, Identity types, Categorical semantics, Homotopy theory ACM Reference Format: ACM Trans. Comput. Logic V, N, Article A (January YYYY), 44 pages. DOI = 10.1145/0000000.0000000 http://doi.acm.org/10.1145/0000000.0000000

• Type: Journal
• Year: 2012
• Where: TOCL
• Authors: Benno van den Berg, Richard Garner
• Keywords: Categorical Semantics, Dependent Type Theory, Formal Methods, Lambda Calculus, TOCL 2012