Smooth and Proper Maps

Mathieu Anel, Jonathan Weinberger

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 theo…