{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,12]],"date-time":"2025-07-12T22:53:06Z","timestamp":1752360786821},"reference-count":10,"publisher":"Springer Science and Business Media LLC","issue":"1-2","license":[{"start":{"date-parts":[[2016,11,1]],"date-time":"2016-11-01T00:00:00Z","timestamp":1477958400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100009244","name":"Stockholm University","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100009244","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Arch. Math. Logic"],"published-print":{"date-parts":[[2017,2]]},"DOI":"10.1007\/s00153-016-0514-7","type":"journal-article","created":{"date-parts":[[2016,11,1]],"date-time":"2016-11-01T06:48:52Z","timestamp":1477982932000},"page":"51-66","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Constructions of categories of setoids from proof-irrelevant families"],"prefix":"10.1007","volume":"56","author":[{"given":"Erik","family":"Palmgren","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,11,1]]},"reference":[{"key":"514_CR1","doi-asserted-by":"crossref","unstructured":"Altenkirch, T.: Extensional equality in intensional type theory. In: 14th Symposium on Logic in Computer Science, pp. 412\u2013421. IEEE Press, Piscataway (1999)","DOI":"10.1109\/LICS.1999.782636"},{"key":"514_CR2","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1017\/S0956796802004501","volume":"13","author":"G Barthe","year":"2003","unstructured":"Barthe, G., Capretta, V., Pons, O.: Setoids in type theory. J. Funct. Program. 13, 261\u2013293 (2003)","journal-title":"J. Funct. Program."},{"key":"514_CR3","volume-title":"Foundations of Constructive Analysis","author":"E Bishop","year":"1967","unstructured":"Bishop, E.: Foundations of Constructive Analysis. McGraw-Hill, New York (1967)"},{"key":"514_CR4","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4471-0963-1","volume-title":"Extensional Concepts in Intensional Type Theory","author":"M Hofmann","year":"1997","unstructured":"Hofmann, M.: Extensional Concepts in Intensional Type Theory. Springer, Berlin (1997)"},{"key":"514_CR5","doi-asserted-by":"crossref","unstructured":"Hofmann, M., Streicher, T.: The groupoid interpretation of type theory. In: Sambin, G., Smith, J. (eds.) Twenty-five years of constructive type theory (Venice, 1995), Oxford Logic Guides, vol. 36, pp.\u00a083\u2013111. Oxford University Press, New York (1998)","DOI":"10.1093\/oso\/9780198501275.003.0008"},{"key":"514_CR6","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1007\/s11787-013-0080-2","volume":"7","author":"ME Maietti","year":"2013","unstructured":"Maietti, M.E., Rosolini, G.: Quotient completion for the foundation of constructive mathematics. Logica Universalis 7, 371\u2013402 (2013)","journal-title":"Logica Universalis"},{"key":"514_CR7","volume-title":"Programming in Martin-L\u00f6f Type Theory","author":"B Nordstr\u00f6m","year":"1990","unstructured":"Nordstr\u00f6m, B., Petersson, K., Smith, J.: Programming in Martin-L\u00f6f Type Theory. Oxford University Press, Oxford (1990)"},{"key":"514_CR8","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1007\/s00153-011-0252-9","volume":"51","author":"E Palmgren","year":"2012","unstructured":"Palmgren, E.: Proof-relevance of families of setoids and identity in type theory. Arch. Math. Log. 51, 35\u201347 (2012)","journal-title":"Arch. Math. Log."},{"key":"514_CR9","doi-asserted-by":"crossref","unstructured":"Palmgren, E., Wilander, O.: Constructing categories and setoids of setoids in type theory. Log. Methods Comput. Sci. 10(3), paper 25 (2014)","DOI":"10.2168\/LMCS-10(3:25)2014"},{"key":"514_CR10","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1017\/S0960129511000478","volume":"22","author":"O Wilander","year":"2012","unstructured":"Wilander, O.: Constructing a small category of setoids. Math. Struct. Comput. Sci. 22, 103\u2013121 (2012)","journal-title":"Math. Struct. Comput. Sci."}],"container-title":["Archive for Mathematical Logic"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00153-016-0514-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00153-016-0514-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00153-016-0514-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,11]],"date-time":"2022-07-11T22:16:48Z","timestamp":1657577808000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00153-016-0514-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,11,1]]},"references-count":10,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2017,2]]}},"alternative-id":["514"],"URL":"https:\/\/doi.org\/10.1007\/s00153-016-0514-7","relation":{},"ISSN":["0933-5846","1432-0665"],"issn-type":[{"value":"0933-5846","type":"print"},{"value":"1432-0665","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,11,1]]}}}