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 $\Sigma$-type and $\Pi$-type constructors of dependent type theory…