{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,13]],"date-time":"2025-05-13T21:57:34Z","timestamp":1747173454437,"version":"3.40.5"},"reference-count":36,"publisher":"Cambridge University Press (CUP)","issue":"2","license":[{"start":{"date-parts":[[2023,6,23]],"date-time":"2023-06-23T00:00:00Z","timestamp":1687478400000},"content-version":"unspecified","delay-in-days":142,"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":[[2023,2]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We show that categories of modules over a ring in homotopy type theory (HoTT) satisfy the internal versions of the AB axioms from homological algebra. The main subtlety lies in proving AB4, which is that coproducts indexed by arbitrary sets are left-exact. To prove this, we replace a set <jats:italic>X<\/jats:italic> with the strict category of lists of elements in <jats:italic>X<\/jats:italic>. From showing that the latter is filtered, we deduce left-exactness of the coproduct. More generally, we show that exactness of filtered colimits (AB5) implies AB4 for any abelian category in HoTT. Our approach is heavily inspired by Roswitha Harting\u2019s construction of the <jats:italic>internal coproduct<\/jats:italic> of abelian groups in an elementary topos with a natural numbers object. To state the AB axioms, we define and study filtered (and sifted) precategories in HoTT. A key result needed is that filtered colimits commute with finite limits of sets. This is a familiar classical result but has not previously been checked in our setting. Finally, we interpret our most central results into an <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0960129523000178_inline1.png\"\/><jats:tex-math>\n$\\infty$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>-topos <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0960129523000178_inline2.png\"\/><jats:tex-math>\n$ {\\mathscr{X}} $\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>. Given a ring <jats:italic>R<\/jats:italic> in <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0960129523000178_inline3.png\"\/><jats:tex-math>\n$ {\\tau_{\\leq 0}({{\\mathscr{X}}})} $\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula> \u2013 for example, an ordinary sheaf of rings \u2013 we show that the internal category of <jats:italic>R<\/jats:italic>-modules in <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0960129523000178_inline4.png\"\/><jats:tex-math>\n$ {\\mathscr{X}} $\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula> represents the presheaf which sends an object <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0960129523000178_inline5.png\"\/><jats:tex-math>\n$ X \\in {\\mathscr{X}} $\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula> to the category of <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0960129523000178_inline6.png\"\/><jats:tex-math>\n$ (X{\\times}R) $\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>-modules in <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0960129523000178_inline7.png\"\/><jats:tex-math>\n${\\mathscr{X}} \/ X$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>. In general, our results yield a product-preserving left adjoint to base change of modules over <jats:italic>X<\/jats:italic>. When <jats:italic>X<\/jats:italic> is 0-truncated, this left adjoint is the internal coproduct. By an internalisation procedure, we deduce left-exactness of the internal coproduct as an ordinary functor from its internal left-exactness coming from HoTT.<\/jats:p>","DOI":"10.1017\/s0960129523000178","type":"journal-article","created":{"date-parts":[[2023,6,23]],"date-time":"2023-06-23T23:23:14Z","timestamp":1687562594000},"page":"106-133","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":0,"title":["Univalent categories of modules"],"prefix":"10.1017","volume":"33","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6670-6928","authenticated-orcid":false,"given":"Jarl G. Taxer\u00e5s","family":"Flaten","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2023,6,23]]},"reference":[{"key":"S0960129523000178_ref24","unstructured":"Rasekh, N. (2021). Univalence in higher category theory. arXiv:2103.12762v2."},{"key":"S0960129523000178_ref21","unstructured":"Martini, L. (2021). Yoneda\u2019s lemma for internal higher categories. arXiv:2103.17141v2."},{"key":"S0960129523000178_ref26","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9947-00-02653-2"},{"volume-title":"Cambridge Tracts in Mathematics","year":"2010","author":"Ad\u00e1mek","key":"S0960129523000178_ref2"},{"key":"S0960129523000178_ref10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73086-6_4"},{"year":"2013","key":"S0960129523000178_ref34"},{"key":"S0960129523000178_ref14","unstructured":"Johnstone, P. T. (1977). Topos Theory, L.M.S. Mathematical Monographs, vol. 10, New York, Academic Press."},{"key":"S0960129523000178_ref6","volume-title":"Encyclopedia of Mathematics and its Applications","volume":"1","author":"Borceux","year":"1994"},{"volume-title":"Symmetry","year":"2023","author":"Bezem","key":"S0960129523000178_ref4"},{"key":"S0960129523000178_ref16","doi-asserted-by":"publisher","DOI":"10.1016\/j.aim.2018.08.003"},{"key":"S0960129523000178_ref8","first-page":"154","article-title":"On truncated quasi-categories","volume":"61","author":"Campbell","year":"2020","journal-title":"Cahiers Topol. G\u00e9om. Diff\u00e9r. Cat\u00e9g."},{"key":"S0960129523000178_ref25","unstructured":"Rasekh, N. (2022). A theory of elementary higher toposes. arXiv:1805.03805v3."},{"key":"S0960129523000178_ref22","unstructured":"nLab authors. (2023). n-truncated object of an (infinity,1)-category. https:\/\/ncatlab.org\/nlab\/show\/n-truncated+object+of+an+(infinity,1)-category. Revision 78."},{"key":"S0960129523000178_ref29","doi-asserted-by":"crossref","unstructured":"Shulman, M. (2017). Elementary $(\\infty,1)$ -topoi. https:\/\/golem.ph.utexas.edu\/category\/2017\/04\/elementary_1topoi.html (visited on 02\/10\/2022).","DOI":"10.4236\/oalib.1103496"},{"key":"S0960129523000178_ref19","doi-asserted-by":"publisher","DOI":"10.1017\/S030500411900015X"},{"key":"S0960129523000178_ref5","unstructured":"Blechschmidt, I. (2018). Flabby and injective objects in toposes. arXiv: 1810.12708v1."},{"key":"S0960129523000178_ref20","doi-asserted-by":"publisher","DOI":"10.1515\/9781400830558"},{"key":"S0960129523000178_ref35","unstructured":"Vergura, M. (2019). Localization theory in an $\\infty$ -topos. arXiv:1907.03836."},{"key":"S0960129523000178_ref32","doi-asserted-by":"publisher","DOI":"10.1017\/S1446788700023685"},{"key":"S0960129523000178_ref12","first-page":"119","article-title":"Sur quelques points d\u2019alg\u00e8bre homologique, I","volume":"9","author":"Grothendieck","year":"1957","journal-title":"Tohoku Mathematical Journal"},{"key":"S0960129523000178_ref1","first-page":"33","article-title":"On sifted colimits and generalized varieties","volume":"2001","author":"Ad\u00e1mek","year":"2001","journal-title":"Theory and Applications of Categories"},{"key":"S0960129523000178_ref36","unstructured":"Voevodsky, V. , Ahrens, B. , Grayson, D. , et al. UniMath \u2014 a computer-checked library of univalent mathematics. Available at https:\/\/unimath.org."},{"key":"S0960129523000178_ref28","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129514000565"},{"key":"S0960129523000178_ref11","unstructured":"de Boer, M. (2020). A Proof and Formalization of the Initiality Conjecture of Dependent Type Theory. Licentiate thesis."},{"key":"S0960129523000178_ref7","doi-asserted-by":"crossref","unstructured":"Buchholtz, U. , van Doorn, F. and Rijke, E. (2018). Higher groups in homotopy type theory. In: Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science.","DOI":"10.1145\/3209108.3209150"},{"key":"S0960129523000178_ref9","unstructured":"Cherradi, E. M. (2022). Interpreting type theory in a quasicategory: a yoneda approach. arXiv: 2207.01967."},{"key":"S0960129523000178_ref13","doi-asserted-by":"publisher","DOI":"10.1080\/00927878208822773"},{"key":"S0960129523000178_ref3","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129514000486"},{"year":"2022","author":"Riehl","key":"S0960129523000178_ref27"},{"key":"S0960129523000178_ref18","article-title":"Notions of Anonymous Existence in Martin-L\u00f6f Type Theory","volume":"13","author":"Kraus","year":"2017","journal-title":"Logical Methods in Computer Science"},{"key":"S0960129523000178_ref23","unstructured":"Rasekh, N. (2018). Complete Segal Objects. arXiv:1805.03561v1."},{"key":"S0960129523000178_ref31","unstructured":"Stenzel, R. (to appear) On notions of compactness, object classifiers and weak Tarski universes. Mathematical Structures in Computer Science arXiv:1911.01895v3."},{"key":"S0960129523000178_ref33","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373824"},{"key":"S0960129523000178_ref30","unstructured":"Shulman, M. (2019). All $(\\infty,1)$ -toposes have strict univalent universes. arXiv:1904.07004."},{"key":"S0960129523000178_ref15","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0061363"},{"key":"S0960129523000178_ref17","doi-asserted-by":"publisher","DOI":"10.4171\/JEMS\/1050"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129523000178","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,7,10]],"date-time":"2023-07-10T09:15:43Z","timestamp":1688980543000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129523000178\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,2]]},"references-count":36,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2023,2]]}},"alternative-id":["S0960129523000178"],"URL":"https:\/\/doi.org\/10.1017\/s0960129523000178","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"type":"print","value":"0960-1295"},{"type":"electronic","value":"1469-8072"}],"subject":[],"published":{"date-parts":[[2023,2]]},"assertion":[{"value":"\u00a9 The Author(s), 2023. 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"}]}}