Smooth and Proper Maps
Category Theory
2025-02-14 v5 Logic in Computer Science
Algebraic Geometry
Logic
Abstract
This is an expository note explaining how the geometric notions of local connectedness and properness are related to the -type and -type constructors of dependent type theory.
Cite
@article{arxiv.2402.00331,
title = {Smooth and Proper Maps},
author = {Mathieu Anel and Jonathan Weinberger},
journal= {arXiv preprint arXiv:2402.00331},
year = {2025}
}
Comments
Dedicated to Andr\'e Joyal to his 80th birthday; 13 pages, 4 tables. v2 simplified Table 3 and corrected the characterization of acyclic/localic maps in the corresponding examples. v3 add more examples. v4 final version before publication, change title, update bibliography. v5 corrected Def. 2.2.1. of the published version. Updated affiliation