{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T16:41:54Z","timestamp":1725727314579},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642389450"},{"type":"electronic","value":"9783642389467"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-38946-7_14","type":"book-chapter","created":{"date-parts":[[2013,5,26]],"date-time":"2013-05-26T21:30:38Z","timestamp":1369603838000},"page":"173-188","source":"Crossref","is-referenced-by-count":7,"title":["Generalizations of Hedberg\u2019s Theorem"],"prefix":"10.1007","author":[{"given":"Nicolai","family":"Kraus","sequence":"first","affiliation":[]},{"given":"Mart\u00edn","family":"Escard\u00f3","sequence":"additional","affiliation":[]},{"given":"Thierry","family":"Coquand","sequence":"additional","affiliation":[]},{"given":"Thorsten","family":"Altenkirch","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"14_CR1","unstructured":"Altenkirch, T., Coquand, T., Escard\u00f3, M., Kraus, N.: On h-propositional reflection and hedbergs theorem (November 2012), \n                    \n                      http:\/\/homotopytypetheory.org\/"},{"key":"14_CR2","unstructured":"Altenkirch, T., Coquand, T., Escard\u00f3, M., Kraus, N.: Constant choice (Agda file), 2012\/2013. Available at the Third-named Author\u2019s Institutional Webpage"},{"key":"14_CR3","unstructured":"Altenkirch, T., Coquand, T., Escard\u00f3, M., Kraus, N.: Generalizations of Hedberg\u2019s theorem (Agda file), 2012\/2013. Available at the Third-named Author\u2019s Institutional Webpage"},{"key":"14_CR4","unstructured":"Awodey, S.: Type theory and homotopy. Technical report (2010)"},{"issue":"4","key":"14_CR5","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1093\/logcom\/14.4.447","volume":"14","author":"S. Awodey","year":"2004","unstructured":"Awodey, S., Bauer, A.: Propositions as (types). Journal of Logic and Computation\u00a014(4), 447\u2013471 (2004)","journal-title":"Journal of Logic and Computation"},{"key":"14_CR6","volume-title":"Implementing Mathematics with the Nurpl Proof Development System","author":"R.L. Constable","year":"1986","unstructured":"Constable, R.L., Allen, S.F., Bromley, H.M., Cleaveland, W.R., Cremer, J.F., Harper, R.W., Howe, D.J., Knoblock, T.B., Mendler, N.P., Panangaden, P., Sasaki, J.T., Smith, S.F.: Implementing Mathematics with the Nurpl Proof Development System. Prentice-Hall, NJ (1986)"},{"issue":"3","key":"14_CR7","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/BF01170929","volume":"38","author":"M.P. Fourman","year":"1982","unstructured":"Fourman, M.P., \u0160\u010dedrov, A.: The \u201cworld\u2019s simplest axiom of choice\u201d fails. Manuscripta Math.\u00a038(3), 325\u2013332 (1982)","journal-title":"Manuscripta Math."},{"key":"14_CR8","doi-asserted-by":"crossref","unstructured":"Hedberg, M.: A coherence theorem for Martin-L\u00f6f\u2019s type theory. J. Functional Programming, 413\u2013436 (1998)","DOI":"10.1017\/S0956796898003153"},{"key":"14_CR9","unstructured":"Hofmann, M., Streicher, T.: The groupoid interpretation of type theory. In: Venice Festschrift, pp. 83\u2013111. Oxford University Press (1996)"},{"key":"14_CR10","unstructured":"Kraus, N.: A direct proof of Hedberg\u2019s theorem. Blog post at homotopytypetheory.org (March 2012)"},{"key":"14_CR11","series-title":"Universitext","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4419-8640-5","volume-title":"A Course in constructive algebra","author":"R. Mines","year":"1988","unstructured":"Mines, R., Richman, F., Ruitenberg, W.: A Course in constructive algebra. Universitext. Springer, New York (1988)"},{"key":"14_CR12","unstructured":"The HoTT and UF community. HoTT github repository"},{"key":"14_CR13","unstructured":"Univalent Foundations Program, IAS. Homotopy Type Theory: Univalent Foundations of Mathematics (2013)"},{"key":"14_CR14","unstructured":"Voevodsky, V.: Coq library. Availabe at the Author\u2019s Institutional Webpage"}],"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-38946-7_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,13]],"date-time":"2019-05-13T03:18:53Z","timestamp":1557717533000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-38946-7_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642389450","9783642389467"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-38946-7_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}