{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,2,17]],"date-time":"2023-02-17T01:10:32Z","timestamp":1676596232195},"reference-count":21,"publisher":"Association for Computing Machinery (ACM)","issue":"1","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2012,1]]},"abstract":"\n In this paper we construct new categorical models for the identity types of Martin-L\u00f6f type theory, in the categories\n Top<\/jats:bold>\n of topological spaces and\n SSet<\/jats:bold>\n of simplicial sets. We do so building on earlier work of Awodey and Warren [2009], which has suggested that a suitable environment for the interpretation of identity types should be a category equipped with a weak factorization system in the sense of Bousfield--Quillen. It turns out that this is not quite enough for a sound model, due to some subtle coherence issues concerned with stability under substitution; and so our first task is to introduce a slightly richer structure, which we call a\n homotopy-theoretic model of identity types<\/jats:italic>\n , and to prove that this is sufficient for a sound interpretation.\n <\/jats:p>\n \n Now, although both\n Top<\/jats:bold>\n and\n SSet<\/jats:bold>\n are categories endowed with a weak factorization system---and indeed, an entire Quillen model structure---exhibiting the additional structure required for a homotopy-theoretic model is quite hard to do. However, the categories we are interested in share a number of common features, and abstracting these leads us to introduce the notion of a\n path object category<\/jats:italic>\n . 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\n Top<\/jats:bold>\n and\n SSet<\/jats:bold>\n , 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.\n <\/jats:p>","DOI":"10.1145\/2071368.2071371","type":"journal-article","created":{"date-parts":[[2012,1,31]],"date-time":"2012-01-31T14:49:20Z","timestamp":1328021360000},"page":"1-44","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":28,"title":["Topological and Simplicial Models of Identity Types"],"prefix":"10.1145","volume":"13","author":[{"given":"Benno","family":"van den Berg","sequence":"first","affiliation":[{"name":"Technische Universit\u00e4t Darmstadt"}]},{"given":"Richard","family":"Garner","sequence":"additional","affiliation":[{"name":"Macquarie University"}]}],"member":"320","published-online":{"date-parts":[[2012,1]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004108001783"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-4049(77)90067-6"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(86)90053-9"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.08.030"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129509007646"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1112\/plms\/pdq026"},{"key":"e_1_2_1_7_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the 8th International Workshop on Computer Science Logic","author":"Hofmann M."},{"key":"e_1_2_1_8_1","volume-title":"Twenty-Five Years of Constructive Type Theory. Oxford Logic Guides Series","volume":"36","author":"Hofmann M."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(09)70129-6"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(93)90169-T"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-4049(96)00165-X"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01220868"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02273-9_14"},{"key":"e_1_2_1_14_1","volume-title":"Programming in Martin-L\u00f6f\u2019s Type Theory. International Series of Monographs on Computer Science Series","volume":"7","author":"Nordstr\u00f6m B."},{"key":"e_1_2_1_15_1","volume-title":"Handbook of Logic in Computer Science","author":"Pitts A. M."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0097438"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-4049(02)00141-X"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1570-7954(96)80019-2"},{"key":"e_1_2_1_19_1","unstructured":"Van Oosten J. 2010. A notion of homotopy for the effective topos. http:\/\/www.staff.science.uu.nl\/∼ooste110. Van Oosten J. 2010. A notion of homotopy for the effective topos. http:\/\/www.staff.science.uu.nl\/∼ooste110."},{"key":"e_1_2_1_20_1","unstructured":"Warren M. 2008. Homotopy theoretic aspects of constructive type theory. Ph.D. thesis Carnegie Mellon University. Warren M. 2008. Homotopy theoretic aspects of constructive type theory. Ph.D. thesis Carnegie Mellon University."},{"key":"e_1_2_1_21_1","unstructured":"Warren M. 2009. A characterization of representable intervals. http:\/\/arxiv.org\/abs\/0903.3743. Warren M. 2009. A characterization of representable intervals. http:\/\/arxiv.org\/abs\/0903.3743."}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2071368.2071371","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,29]],"date-time":"2022-12-29T18:16:32Z","timestamp":1672337792000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2071368.2071371"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,1]]},"references-count":21,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2012,1]]}},"alternative-id":["10.1145\/2071368.2071371"],"URL":"http:\/\/dx.doi.org\/10.1145\/2071368.2071371","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":["Computational Mathematics","Logic","General Computer Science","Theoretical Computer Science"],"published":{"date-parts":[[2012,1]]},"assertion":[{"value":"2010-08-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2010-12-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2012-01-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}