English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT

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;

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.