{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,10]],"date-time":"2026-03-10T12:15:52Z","timestamp":1773144952303,"version":"3.50.1"},"publisher-location":"Dordrecht","reference-count":56,"publisher":"Springer Netherlands","isbn-type":[{"value":"9789400744349","type":"print"},{"value":"9789400744356","type":"electronic"}],"license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-94-007-4435-6_9","type":"book-chapter","created":{"date-parts":[[2012,7,10]],"date-time":"2012-07-10T14:08:37Z","timestamp":1341929317000},"page":"183-201","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":17,"title":["Type Theory and Homotopy"],"prefix":"10.1007","author":[{"given":"Steve","family":"Awodey","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2012,6,7]]},"reference":[{"key":"9_CR1","unstructured":"Aczel, P. 1974. The strength of Martin-L\u00f6f\u2019s type theory with one universe. In Proceedings of the symposium on mathematical logic, Oulu, ed. S. Miettinen and J.J.\u00a0Vaananen, 1\u201332."},{"key":"9_CR2","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1017\/S0305004108001783","volume":"146","author":"S Awodey","year":"2009","unstructured":"Awodey, S., and M.A. Warren. 2009. Homotopy theoretic models of identity types. Mathematical Proceedings of the Cambridge Philosophical Society 146: 45\u201355.","journal-title":"Mathematical Proceedings of the Cambridge Philosophical Society"},{"key":"9_CR3","unstructured":"Awodey, S., P.\u00a0Hofstra, and M.A. Warren. 2009. Martin-L\u00f6f complexes. Submitted, on the arXiv as arXiv:0906.4521."},{"issue":"1","key":"9_CR4","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1006\/aima.1998.1724","volume":"136","author":"MA Batanin","year":"1998","unstructured":"Batanin, M.A. 1998. Monoidal globular categories as a natural environment for the theory of weak n-categories. Advances in Mathematics 136(1): 39\u2013103.","journal-title":"Advances in Mathematics"},{"key":"9_CR5","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/B978-044481779-2\/50002-X","volume-title":"Handbook of algebraic topology","author":"H-J Baues","year":"1995","unstructured":"Baues, H.-J. 1995. Homotopy types. In Handbook of algebraic topology, ed. I.M. James, 1\u201372. Amsterdam: North-Holland."},{"key":"9_CR6","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1016\/0022-4049(77)90067-6","volume":"9","author":"AK Bousfield","year":"1977","unstructured":"Bousfield, A.K. 1977. Constructions of factorization systems in categories. Journal of Pure and Applied Algebra 9: 207\u2013220.","journal-title":"Journal of Pure and Applied Algebra"},{"key":"9_CR7","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1112\/blms\/19.2.113","volume":"19","author":"R Brown","year":"1987","unstructured":"Brown, R. 1987. From groups to groupoids. Bulletin of the London Mathematical Society 19: 113\u2013134.","journal-title":"Bulletin of the London Mathematical Society"},{"issue":"3","key":"9_CR8","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1016\/0168-0072(86)90053-9","volume":"32","author":"J Cartmell","year":"1986","unstructured":"Cartmell, J. 1986. Generalised algebraic theories and contextual categories. Annals of Pure and Applied Logic 32(3): 209\u2013243.","journal-title":"Annals of Pure and Applied Logic"},{"issue":"4","key":"9_CR9","doi-asserted-by":"publisher","first-page":"439","DOI":"10.1007\/s10485-007-9081-8","volume":"15","author":"E Cheng","year":"2007","unstructured":"Cheng, E. 2007. An \u03c9-category with all duals is an \u03c9-groupoid. Applied Categorical Structures 15(4): 439\u2013453.","journal-title":"Applied Categorical Structures"},{"key":"9_CR10","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/B978-044481779-2\/50003-1","volume-title":"Handbook of algebraic topology","author":"WG Dwyer","year":"1995","unstructured":"Dwyer, W.G., and J. Spalinski. 1995. Homotopy theories and model categories. In Handbook of algebraic topology, ed. I.M. James, 73\u2013126. Amsterdam: North-Holland."},{"key":"9_CR11","volume-title":"Lecture notes in computer science","author":"Dybjer, P. 1996. Internal type theory. In Proceedings of the BRA TYPES workshop Torino","year":"1995","unstructured":"Dybjer, P. 1996. Internal type theory. In Proceedings of the BRA TYPES workshop, Torino, June 1995. Lecture notes in computer science, vol. 1158. Berlin: Springer."},{"issue":"3","key":"9_CR12","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., and R. Garner. 2008. The identity type weak factorisation system. Theoretical Computer Science 409(3): 94\u2013109.","journal-title":"Theoretical Computer Science"},{"key":"9_CR13","unstructured":"Garner, R. 2007. Cofibrantly generated natural weak factorisation systems. On the arXiv as math.CT\/0702290."},{"issue":"3","key":"9_CR14","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/s10485-008-9137-4","volume":"17","author":"R Garner","year":"2009","unstructured":"Garner, R. 2009a. Understanding the small object argument. Applied Categorical Structures 17(3): 247\u2013285.","journal-title":"Applied Categorical Structures"},{"issue":"4","key":"9_CR15","doi-asserted-by":"publisher","first-page":"687","DOI":"10.1017\/S0960129509007646","volume":"19","author":"R Garner","year":"2009","unstructured":"Garner, R. 2009b. Two-dimensional models of type theory. Mathematical Structures in Computer Science 19(4): 687\u2013736.","journal-title":"Mathematical Structures in Computer Science"},{"key":"9_CR16","volume-title":"Pursuing stacks","author":"A Grothendieck","year":"1983","unstructured":"Grothendieck, A. 1983. Pursuing stacks. Unpublished letter to Quillen"},{"key":"9_CR17","unstructured":"Hofmann, M. 1995a. Extensional concepts in intensional type theory. Ph.D. thesis, University of Edinburgh."},{"key":"9_CR18","first-page":"427","volume-title":"Computer science logic 1994","author":"M Hofmann","year":"1995","unstructured":"Hofmann, M. 1995b. On the interpretation of type theory in locally cartesian closed categories. In Computer science logic 1994, ed. J. Tiuryn and Leszek Pacholski, 427\u2013441. Berlin\/New York: Springer."},{"key":"9_CR19","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1017\/CBO9780511526619.004","volume-title":"Semantics and logics of computation, Publications of the Newton Institute","author":"M Hofmann","year":"1997","unstructured":"Hofmann, M. 1997. Syntax and semantics of dependent types. In Semantics and logics of computation, Publications of the Newton Institute. ed. P. Dybjer and A.M. Pitts 79\u2013130. Cambridge: Cambridge University Press."},{"key":"9_CR20","first-page":"83","volume-title":"Twenty-five years of constructive type theory. Oxford logic guides","author":"M Hofmann","year":"1995","unstructured":"Hofmann, M., and T.\u00a0Streicher. 1995. The groupoid interpretation of type theory. In Twenty-five years of constructive type theory. Oxford logic guides, vol. 36, ed. G. Sambin and J.\u00a0Smith, 83\u2013111. Oxford: Oxford University Press."},{"key":"9_CR21","volume-title":"Model categories, Mathematical surveys and monographs","author":"M Hovey","year":"1999","unstructured":"Hovey, M. 1999. Model categories, Mathematical surveys and monographs, vol. 63. Providence: American Mathematical Society."},{"key":"9_CR22","first-page":"479","volume-title":"To H. B. Curry: Essays on combinatory logic, lambda Calculus and formalism","author":"WA Howard","year":"1980","unstructured":"Howard, W.A. 1980. The formulae-as-types notion of construction. In To H.\u00a0B. Curry: Essays on combinatory logic, lambda Calculus and formalism, ed. J.P. Seldin and J.R. Hindley, 479\u2013490. London: Academic Press."},{"key":"9_CR23","volume-title":"Categorical logic and type theory","author":"B Jacobs","year":"1999","unstructured":"Jacobs, B. 1999. Categorical logic and type theory. Amsterdam: North-Holland Publishing Co."},{"key":"9_CR24","volume-title":"Sketches of an elephant","author":"PT Johnstone","year":"2003","unstructured":"Johnstone, P.T. 2003. Sketches of an elephant, vol. 2. Oxford: Oxford University Press."},{"key":"9_CR25","unstructured":"Joyal, A. The theory of quasi-categories. In preparation."},{"key":"9_CR26","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1016\/S0022-4049(02)00135-4","volume":"175","author":"A Joyal","year":"2002","unstructured":"Joyal, A. 2002. Quasi-categories and Kan complexes. Journal of Pure and Applied Algebra 175: 207\u2013222.","journal-title":"Journal of Pure and Applied Algebra"},{"key":"9_CR27","volume-title":"An extension of the galois theory of grothendieck, Memoirs of the American Mathematical Society","author":"A Joyal","year":"1984","unstructured":"Joyal, A., and M. Tierney. 1984. An extension of the galois theory of grothendieck, Memoirs of the American Mathematical Society, vol. 51. Providence: American Mathematical Society."},{"key":"9_CR28","doi-asserted-by":"crossref","unstructured":"Joyal, A., and M. Tierney. 1991. Strong stacks and classifying spaces. In Category theory (Como, 1990), Lecture notes in mathematics, vol. 1488, 213\u2013236. Berlin: Springer.","DOI":"10.1007\/BFb0084222"},{"issue":"1","key":"9_CR29","first-page":"29","volume":"32","author":"MM Kapranov","year":"1991","unstructured":"Kapranov, M.M., and V.A. Voevodsky. 1991. \u221e-groupoids and homotopy types. Cahiers de Topologie et G\u00e9ometrie Diff\u00e9rentielle Cat\u00e9goriques 32(1): 29\u201346.","journal-title":"Cahiers de Topologie et G\u00e9ometrie Diff\u00e9rentielle Cat\u00e9goriques"},{"key":"9_CR30","unstructured":"Leinster, T. 2002. A survey of definitions of n-category. Theory and Applications of Categories 10: 1\u201370 (electronic)."},{"key":"9_CR31","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511525896","volume-title":"Higher operads, higher categories, London mathematical society lecture note series","author":"T Leinster","year":"2004","unstructured":"Leinster, T. 2004. Higher operads, higher categories, London mathematical society lecture note series, vol. 298. Cambridge: Cambridge University Press."},{"key":"9_CR32","doi-asserted-by":"crossref","unstructured":"Lumsdaine, P.L. 2009. Weak \u03c9-categories from intensional type theory. In Typed Lambda-calculus and its applications.","DOI":"10.1007\/978-3-642-02273-9_14"},{"key":"9_CR33","doi-asserted-by":"crossref","DOI":"10.1515\/9781400830558","volume-title":"Higher topos theory","author":"J Lurie","year":"2009","unstructured":"Lurie, J. 2009. Higher topos theory. Princeton: Princeton University Press."},{"key":"9_CR34","first-page":"73","volume-title":"Logic Colloquium 73","author":"P Martin-L\u00f6f","year":"1975","unstructured":"Martin-L\u00f6f, P. 1975. An intuitionistic theory of types: Predicative part. In Logic Colloquium 73, ed. H.E. Rose and J.C. Shepherdson, 73\u2013118. Amsterdam: North-Holland."},{"key":"9_CR35","unstructured":"Martin-L\u00f6f, P. 1979. Constructive mathematics and computer programming. In Proceedings of the 6th international congress for logic, methodology and philosophy of science. Amsterdam: North-Holland."},{"key":"9_CR36","volume-title":"Intuitionistic type theory","author":"P Martin-L\u00f6f","year":"1984","unstructured":"Martin-L\u00f6f, P. 1984. Intuitionistic type theory. Napoli: Bibliopolis."},{"key":"9_CR37","doi-asserted-by":"crossref","unstructured":"Martin-L\u00f6f, P. 1998. An intuitionistic theory of types. In Twenty-five years of constructive type theory, Oxford logic guides, vol. 36, ed. G. Sambin and J.\u00a0Smith, 127\u2013172. Oxford: Oxford University Press. This paper was originally a 1972 preprint from the Department of Mathematics at the University of Stockholm.","DOI":"10.1093\/oso\/9780198501275.003.0010"},{"key":"9_CR38","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1016\/S0168-0072(00)00012-9","volume":"104","author":"I Moerdijk","year":"2000","unstructured":"Moerdijk, I., and E.\u00a0Palmgren. 2000. Wellfounded trees in categories. Annals of Pure and Applied Logic 104: 189\u2013218.","journal-title":"Annals of Pure and Applied Logic"},{"key":"9_CR39","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1016\/S0168-0072(01)00079-3","volume":"114","author":"I Moerdijk","year":"2002","unstructured":"Moerdijk, I., and E.\u00a0Palmgren. 2002. Type theories, toposes and constructive set theory: Predicative aspects of AST. Annals of Pure and Applied Logic 114: 155\u2013201.","journal-title":"Annals of Pure and Applied Logic"},{"key":"9_CR40","doi-asserted-by":"crossref","unstructured":"Morel, F., and V.\u00a0Voevodsky. 1999. A\n                  1-homotopy theory of schemes. Publications Math\u00e9matiques de l\u2019I.H.E.S. 90: 45\u2013143.","DOI":"10.1007\/BF02698831"},{"key":"9_CR41","volume-title":"Programming in Martin-L\u00f6f\u2019s type theory. An introduction","author":"B Nordstr\u00f6m","year":"1990","unstructured":"Nordstr\u00f6m, B., K.\u00a0Petersson, and J.M. Smith. 1990. Programming in Martin-L\u00f6f\u2019s type theory. An introduction. Oxford: Oxford University Press."},{"key":"9_CR42","unstructured":"Palmgren, E. 2003. Groupoids and local cartesian closure. Department of Mathematics Technical Report 2003:21, Uppsala University."},{"key":"9_CR43","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0097438","volume-title":"Homotopical algebra, Lecture notes in mathematics","author":"D Quillen","year":"1967","unstructured":"Quillen, D. 1967. Homotopical algebra, Lecture notes in mathematics, vol. 43. Berlin\/Heidelberg: Springer."},{"key":"9_CR44","first-page":"173","volume":"17","author":"E Riehl","year":"2011","unstructured":"Riehl, E. 2011. Algebraic model structures. New York Journal of Mathematics 17: 173\u2013231.","journal-title":"New York Journal of Mathematics"},{"key":"9_CR45","volume-title":"Twenty-five years of constructive type theory, Oxford logic guides, vol. 36","year":"1998","unstructured":"Sambin, G., and J.\u00a0Smith (eds.). 1998. Twenty-five years of constructive type theory, Oxford logic guides, vol. 36. Oxford: Oxford University Press."},{"key":"9_CR46","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1017\/S0305004100061284","volume":"95","author":"RAG Seely","year":"1984","unstructured":"Seely, R.A.G. 1984. Locally cartesian closed categories and type theory. Mathematical Proceedings of the Cambridge Philosophical Society 95: 33\u201348.","journal-title":"Mathematical Proceedings of the Cambridge Philosophical Society"},{"key":"9_CR47","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1016\/S0022-4049(99)00183-8","volume":"154","author":"R Street","year":"2000","unstructured":"Street, R. 2000. The petit topos of globular sets. Journal of Pure and Applied Algebra 154: 299\u2013315.","journal-title":"Journal of Pure and Applied Algebra"},{"key":"9_CR48","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0433-6","volume-title":"Semantics of type theory, Progress in theoretical computer science","author":"T Streicher","year":"1991","unstructured":"Streicher, T. 1991. Semantics of type theory, Progress in theoretical computer science. Basel: Birkhauser."},{"key":"9_CR49","volume-title":"Investigations into intensional type theory","author":"T Streicher","year":"1993","unstructured":"Streicher, T. 1993. Investigations into intensional type theory. Habilitationsschrift, Ludwig-Maximilians-Universit\u00e4t M\u00fcnchen."},{"key":"9_CR50","doi-asserted-by":"crossref","first-page":"28","DOI":"10.1007\/11542384_6","volume-title":"The seventeen provers of the world, Lecture notes in computer Science","author":"L Th\u00e9ry","year":"2006","unstructured":"Th\u00e9ry, L., P.\u00a0Letouzey, and G.\u00a0Gonthier. 2006. Coq. In The seventeen provers of the world, Lecture notes in computer Science, ed. F. Wiedijk, 28\u201335. Berlin\/Heidelberg: Springer."},{"key":"9_CR51","unstructured":"van\u00a0den Berg, B. 2006. Types as weak \u03c9-categories. Lecture delivered in Uppsala, and unpublished notes."},{"key":"9_CR52","doi-asserted-by":"publisher","first-page":"370","DOI":"10.1112\/plms\/pdq026","volume":"102","author":"B van den Berg","year":"2010","unstructured":"van den Berg, B., and R. Garner. 2010. Types are weak \u03c9-groupoids. Proceedings of the London Mathematical Society 102: 370\u2013394","journal-title":"Proceedings of the London Mathematical Society"},{"key":"9_CR53","doi-asserted-by":"crossref","unstructured":"van den Berg, B., and R. Garner. 2012. Topological and simplicial models of identity types. To appear in ACM Transactions on Computational Logic 13(1): 1\u201344.","DOI":"10.1145\/2071368.2071371"},{"key":"9_CR54","volume-title":"A very short note on the homotopy \u03bb-calculus","author":"V Voevodsky","year":"2006","unstructured":"Voevodsky, V. 2006. A very short note on the homotopy \u03bb-calculus. Unpublished note."},{"key":"9_CR55","unstructured":"Warren, M.A. 2008. Homotopy theoretic aspects of constructive type theory. Ph.D. thesis, Carnegie Mellon University."},{"key":"9_CR56","unstructured":"Warren, M. 2010. The strict omega-groupoid interpretation of type theory. Forthcoming in Models, logics and higher-dimensional categories: A tribute to the work of Mih\u00e1ly Makkai. Providence: American Mathematical Society"}],"container-title":["Epistemology versus Ontology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-94-007-4435-6_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,7]],"date-time":"2023-02-07T08:26:25Z","timestamp":1675758385000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-94-007-4435-6_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9789400744349","9789400744356"],"references-count":56,"URL":"https:\/\/doi.org\/10.1007\/978-94-007-4435-6_9","relation":{},"subject":[],"published":{"date-parts":[[2012]]},"assertion":[{"value":"7 June 2012","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}