{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T05:22:22Z","timestamp":1776316942794,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":34,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642216909","type":"print"},{"value":"9783642216916","type":"electronic"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-21691-6_7","type":"book-chapter","created":{"date-parts":[[2011,6,11]],"date-time":"2011-06-11T05:31:26Z","timestamp":1307770286000},"page":"45-60","source":"Crossref","is-referenced-by-count":7,"title":["Homotopy-Theoretic Models of Type Theory"],"prefix":"10.1007","author":[{"given":"Peter","family":"Arndt","sequence":"first","affiliation":[]},{"given":"Krzysztof","family":"Kapulkin","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"7_CR1","unstructured":"Arndt, P., Kapulkin, C.: \u220f- and \u2211-types in homotopy theoretic models of type theory (work in progress)"},{"key":"7_CR2","doi-asserted-by":"crossref","unstructured":"Awodey, S., Warren, M.A.: Homotopy theoretic models of identity types. Math. Proc. of the Cam. Phil. Soc. (2009)","DOI":"10.1017\/S0305004108001783"},{"key":"7_CR3","unstructured":"Awodey, S.: Type theory and homotopy (2010) (preprint)"},{"issue":"2","key":"7_CR4","doi-asserted-by":"publisher","first-page":"245","DOI":"10.4310\/HHA.2010.v12.n2.a9","volume":"12","author":"C. Barwick","year":"2010","unstructured":"Barwick, C.: On left and right model categories and left and right bousfield localizations. Homology, Homotopy and Applications\u00a012(2), 245\u2013320 (2010)","journal-title":"Homology, Homotopy and Applications"},{"issue":"1","key":"7_CR5","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1006\/aima.1998.1724","volume":"136","author":"M.A. Batanin","year":"1998","unstructured":"Batanin, M.A.: Monoidal globular categories as a natural environment for the theory of weak n-categories. Adv. Math.\u00a0136(1), 39\u2013103 (1998)","journal-title":"Adv. Math."},{"issue":"1","key":"7_CR6","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1016\/S0022-4049(01)00176-1","volume":"174","author":"D.-C. Cisinski","year":"2002","unstructured":"Cisinski, D.-C.: Th\u00e9ories homotopiques dans les topos. J. Pure Appl. Algebra\u00a0174(1), 43\u201382 (2002); MR1924082 (2003i:18021)","journal-title":"J. Pure Appl. Algebra"},{"key":"#cr-split#-7_CR7.1","unstructured":"Cisinski, D.-C.: Les pr??faisceaux comme mod??les des types d???homotopie. Ast??risque, (308), xxiv+390 (2006);"},{"key":"#cr-split#-7_CR7.2","unstructured":"MR 2294028 (2007k:55002)"},{"key":"7_CR8","first-page":"891","volume":"A-B 275","author":"F. Conduch\u00e9","year":"1972","unstructured":"Conduch\u00e9, F.: Au sujet de l\u2019existence d\u2019adjoints \u00e0 droite aux foncteurs \u201cimage r\u00e9ciproque\u201d dans la cat\u00e9gorie des cat\u00e9gories. C. R. Acad. Sci. Paris S\u00e9r.\u00a0A-B 275, A891\u2013A894 (1972)","journal-title":"C. R. Acad. Sci. Paris S\u00e9r."},{"key":"7_CR9","unstructured":"Garner, R.: 2-dimensional models of type theory. Mathematical Structures in Computer Science (2008) (to appear)"},{"issue":"1","key":"7_CR10","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1016\/j.tcs.2008.08.030","volume":"409","author":"N. Gambino","year":"2008","unstructured":"Gambino, N., Garner, R.: The identity type weak factorisation system. Theoretical Computer Science\u00a0409(1), 94\u2013109 (2008)","journal-title":"Theoretical Computer Science"},{"key":"7_CR11","unstructured":"Giraud, J.: M\u00e9thode de la descente. M\u00e9moires de la Soc. Math. de France 2 (1964)"},{"key":"7_CR12","unstructured":"Gambino, N., Kock, J.: Polynomial functors and polynomial monads (to appear)"},{"key":"7_CR13","unstructured":"Garner, R., van den Berg, B.: Types are weak \u03c9-groupoids (2008) (submitted)"},{"key":"7_CR14","unstructured":"Garner, R., van den Berg, B.: Topological and simplicial models of identity types (2010) (submitted)"},{"key":"7_CR15","series-title":"Mathematical Surveys and Monographs","volume-title":"Model categories and their localizations","author":"P.S. Hirschhorn","year":"2003","unstructured":"Hirschhorn, P.S.: Model categories and their localizations. Mathematical Surveys and Monographs, vol.\u00a099. American Mathematical Society, Providence (2003), MR 1944041 (2003j:18018)"},{"key":"7_CR16","series-title":"Mathematical Surveys and Monographs","volume-title":"Model categories","author":"M. Hovey","year":"1999","unstructured":"Hovey, M.: Model categories. Mathematical Surveys and Monographs, vol.\u00a063. American Mathematical Society, Providence (1999)"},{"key":"7_CR17","series-title":"Oxford Logic Guides","first-page":"83","volume-title":"Twenty-Five Years of Constructive Type Theory (Venice, 1995)","author":"M. Hofmann","year":"1998","unstructured":"Hofmann, M., Streicher, T.: The groupoid interpretation of type theory. In: Twenty-Five Years of Constructive Type Theory (Venice, 1995). Oxford Logic Guides, vol.\u00a036, pp. 83\u2013111. Oxford Univ. Press, New York (1998)"},{"key":"7_CR18","unstructured":"Kapulkin, C.: Homotopy theoretic models of type theory, Masters Thesis (University of Warsaw) (2010)"},{"key":"7_CR19","series-title":"London Mathematical Society Lecture Note Series","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511525896","volume-title":"Higher operads, higher categories","author":"T. Leinster","year":"2004","unstructured":"Leinster, T.: Higher operads, higher categories. London Mathematical Society Lecture Note Series, vol.\u00a0298. Cambridge University Press, Cambridge (2004)"},{"key":"7_CR20","doi-asserted-by":"crossref","unstructured":"Lumsdaine, P.L.: Weak \u03c9-categories from intensional type theory, extended version (2008)","DOI":"10.1007\/978-3-642-02273-9_14"},{"key":"7_CR21","unstructured":"Lumsdaine, P.L.: Higher categories from type theories, Ph.D. thesis, CMU (2010)"},{"key":"7_CR22","series-title":"Annals of Mathematics Studies","doi-asserted-by":"crossref","DOI":"10.1515\/9781400830558","volume-title":"Higher topos theory","author":"J. Lurie","year":"2009","unstructured":"Lurie, J.: Higher topos theory. Annals of Mathematics Studies, vol.\u00a0170. Princeton University Press, Princeton (2009)"},{"key":"7_CR23","unstructured":"Martin-L\u00f6f, P.: An intuitionstic theory of types, Technical Report, University of Stockholm (1972)"},{"key":"#cr-split#-7_CR24.1","doi-asserted-by":"crossref","unstructured":"Morel, F., Voevodsky, V.: A 1-homotopy theory of schemes. Inst. Hautes ??tudes Sci. Publ. Math. (1999)??(90), 45???143 (2001);","DOI":"10.1007\/BF02698831"},{"key":"#cr-split#-7_CR24.2","unstructured":"MR 1813224 (2002f:14029)"},{"key":"7_CR25","volume-title":"Programming in Martin-L\u00f6f\u2019s type theory","author":"B. Nordstr\u00f6m","year":"1990","unstructured":"Nordstr\u00f6m, B., Petersson, K., Smith, J.M.: Programming in Martin-L\u00f6f\u2019s type theory. Oxford University Press, Oxford (1990)"},{"key":"7_CR26","series-title":"Lecture Notes in Mathematics","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0097438","volume-title":"Homotopical algebra","author":"D. Quillen","year":"1967","unstructured":"Quillen, D.: Homotopical algebra. Lecture Notes in Mathematics, vol.\u00a043. Springer, Heidelberg (1967)"},{"issue":"1","key":"7_CR27","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1016\/S0166-8641(01)00057-8","volume":"119","author":"C. Rezk","year":"2002","unstructured":"Rezk, C.: Every homotopy theory of simplicial algebras admits a proper model. Topology Appl.\u00a0119(1), 65\u201394 (2002); MR 1881711 (2003g:55033)","journal-title":"Topology Appl."},{"issue":"1","key":"7_CR28","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1017\/S0305004100061284","volume":"95","author":"R.A.G. Seely","year":"1984","unstructured":"Seely, R.A.G.: Locally cartesian closed categories and type theory. Math. Proc. Cambridge Philos. Soc.\u00a095(1), 33\u201348 (1984)","journal-title":"Math. Proc. Cambridge Philos. Soc."},{"key":"7_CR29","series-title":"Studies in Logic and the Foundations of Mathematics","volume-title":"Lectures on Curry\u2013Howard isomorphism","author":"M.H. S\u00f8rensen","year":"2006","unstructured":"S\u00f8rensen, M.H., Urzyczyn, P.: Lectures on Curry\u2013Howard isomorphism. Studies in Logic and the Foundations of Mathematics, vol.\u00a0149. Eslevier, Amsterdam (2006)"},{"key":"#cr-split#-7_CR30.1","doi-asserted-by":"crossref","unstructured":"Voevodsky, V.: $\\bold A^1$ -homotopy theory. In: Proceedings of the International Congress of Mathematicians, Berlin, vol.??I, pp. 579???604 (electronic) (1998);","DOI":"10.4171\/dms\/1-1\/21"},{"key":"#cr-split#-7_CR30.2","unstructured":"MR 1648048 (99j:14018)"},{"key":"7_CR31","unstructured":"Warren, M.A.: Homotopy theoretic aspects of constructive type theory, Ph.D. thesis, CMU (2008)"}],"container-title":["Lecture Notes in Computer Science","Typed Lambda Calculi and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-21691-6_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,7]],"date-time":"2023-06-07T09:37:49Z","timestamp":1686130669000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-21691-6_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642216909","9783642216916"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-21691-6_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}