Within dependent type theory, we provide a topological counterpart of well-founded trees (for short, W-types) by using a proof-relevant version of the notion of inductively generated suplattices introduced in the context of formal topology under the name of inductively generated basic covers. In more detail, we show, firstly, that in Homotopy Type Theory, W-types and proof relevant inductively generated basic covers are propositionally mutually encodable. Secondly, we prove they are definitionally mutually encodable in the Agda implementation of intensional Martin-Loef's type theory. Finally, we reframe the equivalence in the Minimalist Foundation framework by introducing well-founded predicates as the logical counterpart for predicates of dependent W-types. All the results have been checked in the Agda proof-assistant.

翻译：在依赖类型理论内，我们通过使用形式拓扑中称为归纳生成基本覆盖的、以证明相关版本的概念（该概念最初在形式拓扑的背景下以“归纳生成基本覆盖”之名引入）来为良基树（简称W-类型）提供拓扑对应。具体而言，我们首先证明，在同伦类型理论中，W-类型与证明相关的归纳生成基本覆盖在命题层面上可相互编码。其次，我们证明它们在内涵Martin-Löf类型理论的Agda实现中是可定义地相互编码的。最后，我们通过将良基谓词作为依赖W-类型谓词的逻辑对应引入，在最小主义基础框架中重新构建这一等价关系。所有结果均已在Agda证明辅助工具中得到检验。