Smooth and Proper Maps

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