Smooth and proper maps with respect to a fibration

Anel, Mathieu; Weinberger, Jonathan

doi:10.1017/S096012952400032X

Item

ITEM ACTIONSEXPORT

Add to Basket

Local TagsRelease HistoryDetailsSummary

Released

Journal Article

Smooth and proper maps with respect to a fibration

MPS-Authors

/persons/resource/persons297260

Weinberger, Jonathan
Max Planck Institute for Mathematics, Max Planck Society;

External Resource

https://doi.org/10.48550/arXiv.2402.00331
(Preprint)

https://doi.org/10.1017/S096012952400032X
(Publisher version)

Fulltext (restricted access)

There are currently no full texts shared for your IP range.

Fulltext (public)

2402.00331.pdf
(Preprint), 253KB

Supplementary Material (public)

There is no public supplementary material available

Citation

Anel, M., & Weinberger, J. (in press). Smooth and proper maps with respect to a fibration. Mathematical Structures in Computer Science, Published Online - Print pending. doi:10.1017/S096012952400032X.

Cite as: https://hdl.handle.net/21.11116/0000-000F-5497-8

Abstract

This paper explain how the geometric notions of local contractibility and properness are related to the Σ-types and Π-types constructors of dependent type theory. We shall see how every Grothendieck fibration comes canonically with such a pair of notions—called smooth and proper maps—and 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.