{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,12]],"date-time":"2025-02-12T05:25:02Z","timestamp":1739337902255,"version":"3.37.0"},"reference-count":41,"publisher":"Cambridge University Press (CUP)","issue":"9","license":[{"start":{"date-parts":[[2024,11,6]],"date-time":"2024-11-06T00:00:00Z","timestamp":1730851200000},"content-version":"unspecified","delay-in-days":36,"URL":"https:\/\/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>This paper explain how the geometric notions of local contractibility and properness are related to the <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S096012952400032X_inline1.png\"\/><jats:tex-math>\n$\\Sigma$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>-types and <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S096012952400032X_inline2.png\"\/><jats:tex-math>\n$\\Pi$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>-types constructors of dependent type theory. We shall see how every Grothendieck fibration comes canonically with such a pair of notions\u2014called smooth and proper maps\u2014and how this recovers the previous examples and many more. This paper uses category theory to reveal a common structure between geometry and logic, with the hope that the parallel will be beneficial to both fields. The style is mostly expository, and the main results are proved in external references.<\/jats:p>","DOI":"10.1017\/s096012952400032x","type":"journal-article","created":{"date-parts":[[2024,11,6]],"date-time":"2024-11-06T04:35:38Z","timestamp":1730867738000},"page":"971-984","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":0,"title":["Smooth and proper maps with respect to a fibration"],"prefix":"10.1017","volume":"34","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6735-3340","authenticated-orcid":false,"given":"Mathieu","family":"Anel","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4701-3207","authenticated-orcid":false,"given":"Jonathan","family":"Weinberger","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2024,11,6]]},"reference":[{"key":"S096012952400032X_ref22","doi-asserted-by":"publisher","DOI":"10.1090\/pspum\/017\/0257175"},{"key":"S096012952400032X_ref37","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19830291005"},{"key":"S096012952400032X_ref31","doi-asserted-by":"publisher","DOI":"10.1090\/memo\/0705"},{"key":"S096012952400032X_ref25","unstructured":"Lurie, J. (2017). Spectral algebraic geometry. version of February 3 Online book."},{"key":"S096012952400032X_ref41","doi-asserted-by":"publisher","DOI":"10.1016\/j.jpaa.2024.107659"},{"key":"S096012952400032X_ref28","unstructured":"Martini, L. and Wolf, S. (2023a). Internal higher topos theory, arXiv: 2303.06437."},{"key":"S096012952400032X_ref4","doi-asserted-by":"crossref","unstructured":"Anel, M. , Biedermann, G. , Finster, E. and Joyal, A. (2023). Left-exact localizations of \u221e-topoi III: Acyclic Product. Preprint. arXiv: 2308.15573.","DOI":"10.1016\/j.aim.2022.108268"},{"key":"S096012952400032X_ref29","unstructured":"Martini, L. and Wolf, S. (2023b). Proper morphisms of \u221e-topoi , arXiv: 2311.08051."},{"key":"S096012952400032X_ref33","doi-asserted-by":"publisher","DOI":"10.1112\/blms.12997"},{"key":"S096012952400032X_ref20","doi-asserted-by":"publisher","DOI":"10.1016\/0022-4049(82)90083-4"},{"key":"S096012952400032X_ref21","unstructured":"Joyal, A. (2020). Notes on clans and tribes. arXiv: 1710.10238."},{"volume-title":"Cambridge Studies in Advanced Mathematics","year":"2019","author":"Cisinski","key":"S096012952400032X_ref12"},{"key":"S096012952400032X_ref17","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0084217"},{"year":"1986","author":"Rosolini","key":"S096012952400032X_ref36"},{"key":"S096012952400032X_ref2","doi-asserted-by":"publisher","DOI":"10.1112\/topo.12163"},{"key":"S096012952400032X_ref10","doi-asserted-by":"crossref","first-page":"74","DOI":"10.21136\/HS.2023.04","article-title":"Synthetic fibered (\u221e,1)-category theory","volume":"7","author":"Buchholtz","year":"2023","journal-title":"Higher Structures"},{"key":"S096012952400032X_ref35","article-title":"Modalities in homotopy type theory","volume":"16","author":"Rijke","year":"2019","journal-title":"Logical Methods in Computer Science"},{"key":"S096012952400032X_ref34","doi-asserted-by":"publisher","DOI":"10.21136\/HS.2017.06"},{"key":"S096012952400032X_ref16","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-02541-3"},{"key":"S096012952400032X_ref3","doi-asserted-by":"publisher","DOI":"10.1016\/j.aim.2022.108268"},{"key":"S096012952400032X_ref7","unstructured":"Anel, M. and Lejay, D. (2019). Exponentiable \u221e-topoi (version 2), Preprint on Anel\u2019s homepage. http:\/\/mathieu.anel.free.fr\/mat\/doc\/Anel-Lejay-Exponentiable-topoi.pdf"},{"key":"S096012952400032X_ref24","doi-asserted-by":"publisher","DOI":"10.1515\/9781400830558"},{"key":"S096012952400032X_ref27","unstructured":"Martini, L. (2022). Cocartesian fibrations and straightening internal to an \u221e-Topos. arXiv: 2204.00295."},{"key":"S096012952400032X_ref23","doi-asserted-by":"publisher","DOI":"10.1111\/j.1746-8361.1969.tb01194.x"},{"key":"S096012952400032X_ref11","first-page":"831","article-title":"Th\u00e9ories relatives \u00e0 un corpus","volume":"281","author":"B\u00e9nabou","year":"1975","journal-title":"Comptes Rendus de l\u2019Acad\u00e9mie des Sciences de Paris"},{"key":"S096012952400032X_ref1","unstructured":"Joyal, A. (2008). Notes on Quasicategories. On P. May\u2019s homepage. https:\/\/www.math.uchicago.edu\/~may\/IMA\/Joyal.pdf"},{"key":"S096012952400032X_ref13","unstructured":"Escard\u00f3, M. (2004). Topology via higher-order intuitionistic logic. Lecture Notes at MFPS in Pittsburgh. On Escard\u00f3\u2019s website."},{"key":"S096012952400032X_ref15","unstructured":"Escard\u00f3, M. (2020). Intersections of compactly many open sets are open. arXiv: 2001.06050."},{"first-page":"155","year":"2021","author":"Anel","key":"S096012952400032X_ref6"},{"key":"S096012952400032X_ref39","unstructured":"Streicher, T. (2018) Fibered categories \u00e0 la B\u00e9nabou, Lecture notes arXiv: 1801.0.2927."},{"volume-title":"Stone Spaces","year":"1982","author":"Johnstone","key":"S096012952400032X_ref18"},{"key":"S096012952400032X_ref26","first-page":"1","volume-title":"Structures d\u2032asph\u00e9ricit\u00e9, foncteurs lisses, et fibrations","author":"Maltsiniotis","year":"2005"},{"key":"S096012952400032X_ref8","doi-asserted-by":"publisher","DOI":"10.21136\/HS.2020.05"},{"key":"S096012952400032X_ref9","doi-asserted-by":"publisher","DOI":"10.1016\/j.jpaa.2015.06.002"},{"volume-title":"Sketches of an Elephant: A Topos Theory Compendium","year":"2002","author":"Johnstone","key":"S096012952400032X_ref19"},{"year":"1982","author":"Moens","key":"S096012952400032X_ref30"},{"key":"S096012952400032X_ref38","unstructured":"Shulman, M. and All, (2019). (\u221e,1)-toposes have strict univalent universes . arXiv: 1904.07004."},{"key":"S096012952400032X_ref5","doi-asserted-by":"publisher","DOI":"10.1016\/j.jpaa.2023.107472"},{"key":"S096012952400032X_ref32","doi-asserted-by":"publisher","DOI":"10.1090\/noti2692"},{"key":"S096012952400032X_ref40","unstructured":"Weinberger, J. (2022) Strict stability of extension types, arXiv: 2203.07194."},{"key":"S096012952400032X_ref14","first-page":"21","article-title":"Synthetic topology: of data types and classical spaces","volume":"87","author":"Escard\u00f3","year":"2004","journal-title":"Electronic Notes in Theoretical Computer Science"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S096012952400032X","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,11]],"date-time":"2025-02-11T11:35:06Z","timestamp":1739273706000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S096012952400032X\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10]]},"references-count":41,"journal-issue":{"issue":"9","published-print":{"date-parts":[[2024,10]]}},"alternative-id":["S096012952400032X"],"URL":"https:\/\/doi.org\/10.1017\/s096012952400032x","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"type":"print","value":"0960-1295"},{"type":"electronic","value":"1469-8072"}],"subject":[],"published":{"date-parts":[[2024,10]]},"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 (https:\/\/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"}]}}