依赖类型论中归纳与共归纳定义的拓扑解读
A topological reading of inductive and coinductive definitions in Dependent Type Theory
AI总结：
本文在依赖类型论中用共归纳生成的正性关系刻画共归纳谓词，并联系良基树的形式覆盖拓扑解释，全部证明已在 Agda 中形式化。
摘要：
在依赖类型论语境下，我们证明共归纳谓词具有一个等价的拓扑对应物，即共归纳生成的正性关系；该关系由 G. Sambin 提出，用于在无点拓扑中表示闭子集。我们的工作是对先前与 M.E. Maietti 合作研究的补充；在那项研究中，我们证明在依赖类型论中，众所周知的良基树概念具有一个拓扑等价对应物，即与证明相关的归纳生成形式覆盖，用于给出完备上半格的直谓且构造性表示。Martin-Löf 类型论中的所有证明均已在 Agda 证明助手中形式化。
英文摘要：
In the context of dependent type theory, we show that coinductive predicates have an equivalent topological counterpart in terms of coinductively generated positivity relations, introduced by G. Sambin to represent closed subsets in point-free topology. Our work is complementary to a previous one with M.E. Maietti, where we showed that, in dependent type theory, the well-known concept of wellfounded trees has a topological equivalent counterpart in terms of proof-relevant inductively generated formal covers used to provide a predicative and constructive representation of complete suplattices. All proofs in Martin-Löf's type theory are formalised in the Agda proof assistant.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
