Agda中逐点相等≗与命题相等≡的对比及相关问题

我在基于列表证明函数性质时，需要证明该性质在列表的map操作下保持不变。在Agda标准库中找到了实用的同余证明map-cong，其代码如下：

map-cong : ∀ {f g : A → B} → f ≗ g → map f ≗ map g
map-cong f≗g []       = refl
map-cong f≗g (x ∷ xs) = cong₂ _∷_ (f≗g x) (map-cong f≗g xs)

我希望用命题相等≡完成证明，但map-cong证明的是逐点相等≗，因此有以下问题：

• 我注意到map-cong最初基于≡实现，后来被泛化，这说明≗是≡的泛化。有没有办法从逐点相等推导出命题相等，比如存在函数f ≗ g → f ≡ g？
• 从实现来看，逐点相等似乎是通过外延公理定义为函数的命题相等：若两个函数对所有输入都返回相同结果，则它们相等。map-cong的定义既匹配证明f≗g也匹配输入参数，印证了这一点。我的理解是否正确？有没有关于≗实现的文档或说明？我发现标准库中的实现没有文档，还比较复杂，分散在多个文件里，用了多层抽象。
• 除了浏览源码（比如用grep或在GitHub里点看），有没有更便捷的方式浏览Agda标准库？

问题解答 #

1. 从逐点相等推导命题相等 #

在Agda的核心理论中，函数外延性就是你要找的公理：它断言如果两个函数逐点相等（f ≗ g），那么它们命题相等（f ≡ g）。这个公理并非Agda内置，但标准库提供了相关支持，你可以从Function.Extensionality模块导入extensionality或≗-implies-≡。

需要注意的是，函数外延性在构造性类型论中并非默认成立，属于可选公理。如果依赖它，证明会带上该公理的假设。

2. 逐点相等≗的定义与理解 #

你的理解完全正确：逐点相等≗的核心就是“对所有输入，函数输出相等”。在Agda标准库中，它的基础定义通常是：

_≗_ : ∀ {A B : Set} → (A → B) → (A → B) → Set
f ≗ g = ∀ x → f x ≡ g x

这个定义确实分散在多个模块中（比如Function.Base或Relation.Binary.PropositionalEquality的子模块），因为标准库会把通用关系抽象分层组织。目前标准库的文档确实不够完善，但你可以重点查看Function.Base和Relation.Binary下的模块，那里集中了函数相等相关的定义。

3. 便捷浏览Agda标准库的方式 #

除了直接查看源码，还有几种更高效的方式：

• 生成HTML文档：运行标准库根目录的make html命令，生成本地HTML文档后，可通过网页导航查看模块结构和定义，比纯源码更易读。
• IDE跳转功能：在VS Code或Emacs的Agda插件中，按住Ctrl（或Cmd）点击符号（比如≗），可直接跳转到其定义位置，还能查看相关依赖。
• 社区资源：一些Agda教程（如《Programming Language Foundations in Agda》）会附带标准库核心模块的讲解，部分社区论坛也有对标准库常用模块的整理说明。

内容的提问来源于stack exchange，提问作者PaulProgrammerNoob