{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,5,1]],"date-time":"2022-05-01T11:25:12Z","timestamp":1651404312904},"reference-count":31,"publisher":"Cambridge University Press (CUP)","issue":"5","license":[{"start":{"date-parts":[[2015,2,20]],"date-time":"2015-02-20T00:00:00Z","timestamp":1424390400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2015,6]]},"abstract":"<jats:p>We present an interpretation of a version of dependent type theory where a type is interpreted by a Kan semisimplicial set. This interprets only a weak notion of conversion similar to the one used in the first published version of Martin-L\u00f6f type theory. Each truncated version of this model can be carried out internally in dependent type theory, and we have formalized the first truncated level, which is enough to represent isomorphisms of algebraic structure as equality.<\/jats:p>","DOI":"10.1017\/s0960129514000504","type":"journal-article","created":{"date-parts":[[2015,2,20]],"date-time":"2015-02-20T05:16:13Z","timestamp":1424409373000},"page":"1071-1099","source":"Crossref","is-referenced-by-count":4,"title":["A generalization of the Takeuti\u2013Gandy interpretation"],"prefix":"10.1017","volume":"25","author":[{"given":"BRUNO","family":"BARRAS","sequence":"first","affiliation":[]},{"given":"THIERRY","family":"COQUAND","sequence":"additional","affiliation":[]},{"given":"SIMON","family":"HUBER","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2015,2,20]]},"reference":[{"key":"S0960129514000504_ref17","doi-asserted-by":"crossref","unstructured":"Licata D. and Harper R. (2012) Canonicity for 2-dimensional type theory. In: POPL '12: Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ACM 337\u2013348.","DOI":"10.1145\/2103656.2103697"},{"key":"S0960129514000504_ref5","unstructured":"Bezem M. and Coquand Th. (2013) A Kripke model for simplicial sets. Preprint."},{"key":"S0960129514000504_ref29","doi-asserted-by":"crossref","first-page":"39","DOI":"10.4099\/jjm1924.23.0_39","article-title":"On a generalized logic calculus","volume":"23","author":"Takeuti","year":"1953","journal-title":"Japanese Journal of Mathematics"},{"key":"S0960129514000504_ref24","doi-asserted-by":"publisher","DOI":"10.1007\/s00153-011-0252-9"},{"key":"S0960129514000504_ref19","unstructured":"Martin-L\u00f6f P. (1972) An intuitionistic theory of types. In: Sambin G. and Smith J. (eds.) published in the volume 25 Years of Type Theory"},{"key":"S0960129514000504_ref18","unstructured":"Martin-L\u00f6f P. (1971) Haupsatz for intuitionistic simple type theory. In: Proceeding of the Fourth International congress for Logic, Methodology, and Philosophy of Science, Bucharest, 279\u2013290."},{"key":"S0960129514000504_ref27","unstructured":"Streicher T. (2011) A model of type theory in simplicial sets. Unpublished notes available at the author's home page http:\/\/www.mathematik.tu-darmstadt.de\/~streicher\/sstt.pdf."},{"key":"S0960129514000504_ref12","doi-asserted-by":"publisher","DOI":"10.2307\/2268484"},{"key":"S0960129514000504_ref9","first-page":"579","volume-title":"H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","author":"De Bruijn","year":"1980"},{"key":"S0960129514000504_ref14","volume-title":"Simplicial Homotopy Theory","author":"Goerss","year":"1997"},{"key":"S0960129514000504_ref26","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(85)80001-2"},{"key":"S0960129514000504_ref31","doi-asserted-by":"crossref","unstructured":"Voevodsky V. (2010) Univalent foundations project. NSF grant application.","DOI":"10.1007\/978-3-642-20920-8_4"},{"key":"S0960129514000504_ref25","doi-asserted-by":"publisher","DOI":"10.2307\/2369962"},{"key":"S0960129514000504_ref7","volume-title":"Foundations of Constructive Analysis","author":"Bishop","year":"1967"},{"key":"S0960129514000504_ref10","doi-asserted-by":"publisher","DOI":"10.3406\/rhs.1988.4094"},{"key":"S0960129514000504_ref3","doi-asserted-by":"crossref","unstructured":"Altenkirch T. , McBride C. and Swierstra W. (2007) Observational equality, now! In: PLPV '07: Proceedings of the 2007 Workshop on Programming Languages Meets Program Verification, ACM 57\u201368.","DOI":"10.1145\/1292597.1292608"},{"key":"S0960129514000504_ref13","doi-asserted-by":"crossref","unstructured":"Girard J. Y. (1971) Une extension de l'interpr\u00e9tation de G\u00f6del \u00e0 l'analyse et son application \u00e0 l'\u00e9limination des coupures dans l'analyse et la th\u00e9orie des types. In: J. E. Fenstad (ed.) Proceedings of the Second Scandinavian Logic Symposium, North-Holland 63\u201392.","DOI":"10.1016\/S0049-237X(08)70843-7"},{"key":"S0960129514000504_ref2","doi-asserted-by":"crossref","unstructured":"Altenkirch T. (1999) Extensional equality in intensional type theory. In: 14th Symposium on Logic in Computer Science, 412\u2013420.","DOI":"10.1109\/LICS.1999.782636"},{"key":"S0960129514000504_ref6","unstructured":"Bezem M. , Coquand Th. and Huber S. (2014) A model of type theory in cubical sets. In: R. Matthes and A. Schubert (eds.) Proceedings of the 19th International Conference on Types for Proofs and Programs (TYPES 2013), Dagstuhl, Germany, 107\u2013128."},{"key":"S0960129514000504_ref4","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004108001783"},{"key":"S0960129514000504_ref23","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4419-8640-5"},{"key":"S0960129514000504_ref8","doi-asserted-by":"publisher","DOI":"10.2307\/2266170"},{"key":"S0960129514000504_ref22","unstructured":"May P. (1967) Simplicial Objects in Algebraic Topology, Van Norstrand."},{"key":"S0960129514000504_ref20","unstructured":"Martin-L\u00f6f P. (1973) An intuitionistic theory of types: Predicative part. Logic Colloquium, 73\u2013118."},{"key":"S0960129514000504_ref30","volume-title":"Constructivism in Mathematics. An Introduction","author":"Troelstra","year":"1988"},{"key":"S0960129514000504_ref21","doi-asserted-by":"crossref","unstructured":"Martin-L\u00f6f P. (1975) About models for intuitionistic type theories and the notion of definitional equality. In: Proceedings of the Third Scandinavian Symposium, North-Holland.","DOI":"10.1016\/S0049-237X(08)70727-4"},{"key":"S0960129514000504_ref16","unstructured":"Kapulkin C. , Lumsdaine P. L. and Voevodsky V. (2012) The simplicial model of univalent foundations. Preprint, http:\/\/arxiv.org\/abs\/1211.2851."},{"key":"S0960129514000504_ref11","unstructured":"Gandy R. (1953) On Axiomatic Systems in Mathematics and Theories in Physics, Ph.D. thesis, University of Cambridge."},{"key":"S0960129514000504_ref15","unstructured":"Hofmann M. (1994) Extensional Concepts in Intensional Type Theory, Ph.D. thesis, Edinburgh."},{"key":"S0960129514000504_ref28","doi-asserted-by":"publisher","DOI":"10.2307\/2271658"},{"key":"S0960129514000504_ref1","first-page":"55","article-title":"The type theoretic interpretation of constructive set theory","volume":"77","author":"Aczel","year":"1978","journal-title":"Logic Colloquium"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129514000504","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,20]],"date-time":"2019-08-20T23:30:32Z","timestamp":1566343832000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129514000504\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,2,20]]},"references-count":31,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2015,6]]}},"alternative-id":["S0960129514000504"],"URL":"https:\/\/doi.org\/10.1017\/s0960129514000504","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,2,20]]}}}