{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,20]],"date-time":"2026-04-20T22:41:41Z","timestamp":1776724901669,"version":"3.51.2"},"reference-count":0,"publisher":"Cambridge University Press (CUP)","issue":"9","license":[{"start":{"date-parts":[[2024,9,19]],"date-time":"2024-09-19T00:00:00Z","timestamp":1726704000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2024,10]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We take another look at the construction by Hofmann and Streicher of a universe <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0960129524000203_inline1.png\"\/><jats:tex-math>\n$(U,{\\mathcal{E}l})$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula> for the interpretation of Martin-L\u00f6f type theory in a presheaf category <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0960129524000203_inline2.png\"\/><jats:tex-math>\n$[{{{\\mathbb{C}}}^{\\textrm{op}}},\\textsf{Set}]$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>. It turns out that <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0960129524000203_inline3.png\"\/><jats:tex-math>\n$(U,{\\mathcal{E}l})$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula> can be described as the <jats:italic>nerve<\/jats:italic> of the classifier <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0960129524000203_inline4.png\"\/><jats:tex-math>\n$\\dot{{\\textsf{Set}}}^{\\textsf{op}} \\rightarrow{{\\textsf{Set}}}^{\\textsf{op}}$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula> for discrete fibrations in <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0960129524000203_inline5.png\"\/><jats:tex-math>\n$\\textsf{Cat}$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>, where the nerve functor is right adjoint to the so-called \u201cGrothendieck construction\u201d taking a presheaf <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0960129524000203_inline6.png\"\/><jats:tex-math>\n$P :{{{\\mathbb{C}}}^{\\textrm{op}}}\\rightarrow{\\textsf{Set}}$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula> to its category of elements <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0960129524000203_inline7.png\"\/><jats:tex-math>\n$\\int _{\\mathbb{C}} P$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>. We also consider change of base for such universes, as well as universes of structured families, such as fibrations.<\/jats:p>","DOI":"10.1017\/s0960129524000203","type":"journal-article","created":{"date-parts":[[2024,9,19]],"date-time":"2024-09-19T10:00:41Z","timestamp":1726740041000},"page":"894-910","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":6,"title":["On Hofmann\u2013Streicher universes"],"prefix":"10.1017","volume":"34","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9005-179X","authenticated-orcid":false,"given":"Steve","family":"Awodey","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2024,9,19]]},"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129524000203","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,11]],"date-time":"2025-02-11T11:35:03Z","timestamp":1739273703000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129524000203\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,9,19]]},"references-count":0,"journal-issue":{"issue":"9","published-print":{"date-parts":[[2024,10]]}},"alternative-id":["S0960129524000203"],"URL":"https:\/\/doi.org\/10.1017\/s0960129524000203","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,9,19]]},"assertion":[{"value":"\u00a9 The Author(s), 2024. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (http:\/\/creativecommons.org\/licenses\/by\/4.0\/), which permits unrestricted re-use, distribution and reproduction, provided the original article is properly cited.","name":"license","label":"License","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}