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.

翻译：本文是一篇阐述性笔记，旨在解释局部连通性与恰当性这两个几何概念如何与依值类型论中的 $\Sigma$-类型和 $\Pi$-类型构造子相关联。