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.

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