Smooth and Proper Maps

Abstract

This is an expository note explaining how the geometric notions of local connectedness and properness are related to the $\hat{I}\pounds$-type and $\hat{I}$-type constructors of dependent type theory.

Dedicated to André 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