如何在Agda中证明函数式map-foo具有内射性？

要证明map-foo-injective，核心依赖函数外延性和record构造子的单射特性，以下是具体实现步骤：

必要模块导入 #

Agda默认不内置函数外延性，需显式引入或假设：

open import Relation.Binary.PropositionalEquality
open import Function.Extensionality using (Extensionality)
-- 假设函数外延性成立
postulate ext : ∀ {A B : Set} → Extensionality A B

完整证明代码 #

record Foo (A : Set) : Set where
  constructor foo
  field
    foo-a : A

map-foo : forall {A} -> (A -> A) -> Foo A -> Foo A
map-foo f (foo a) = foo (f a)

map-foo-injective : forall {A} {f g : A -> A} ->  map-foo f ≡ map-foo g -> f ≡ g
map-foo-injective {A} {f} {g} eq = ext λ a → 
  cong Foo.foo-a (cong (_$ foo a) eq)

证明思路拆解 #

1. 应用等式到具体参数：用cong (_$ foo a) eq将map-foo f ≡ map-foo g这个函数等式作用到foo a上，得到map-foo f (foo a) ≡ map-foo g (foo a)，展开后即为foo (f a) ≡ foo (g a)。
2. 提取内层等价关系：通过cong Foo.foo-a对等式两边应用record的投影函数Foo.foo-a——由于Foo.foo-a (foo x)直接返回x，因此得到f a ≡ g a。
3. 函数外延性推广：借助ext（函数外延性公理），从“对任意a都有f a ≡ g a”推导出函数层面的等价f ≡ g。

补充说明 #

如果无法直接导入Function.Extensionality，可以直接通过postulate声明函数外延性：

postulate
  fun-ext : ∀ {A B : Set} {f g : A → B} → (∀ x → f x ≡ g x) → f ≡ g

此时证明可改写为：

map-foo-injective {A} {f} {g} eq = fun-ext λ a → 
  cong Foo.foo-a (cong (_$ foo a) eq)

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