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.

翻译：这篇说明性笔记解释了局部连通性和固有性这两个几何概念如何与依赖类型理论中的 Σ-类型与 Π-类型构造子相关联。