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.

翻译：这是一篇说明性短文，阐释局部连通性和固有性这些几何概念如何与依赖类型论中的∑-类型和∏-类型构造子相关联。