函数外延性

函数外延性指函数类型的性质, 说的是 “两函数相等当且仅当它们对每个参数返回相同的输出”.

该性质独立于使用 J 公理作为相等类型消去规则的 Martin-Löf 类型论, 在同伦类型论中是泛等公理的推论、立方类型论和观测类型论中是定理.

1定义

参见: 函数类型

简单定义

如下是最容易理解, 也是最常见的函数外延性定义.

定义 1.1. 函数外延性指如下类型的实例: 对于函数 $f,g:A\to B$, $$\mathrm{funExt}:\left(\prod _{a:A}{\mathrm{Id}}_B(f(a),g(a))\right)\to {\mathrm{Id}}_{A\to B}(f,g)$$

以上定义仅针对简单类型的函数, 还有$\Pi$ 类型的版本:

定义 1.2. 函数外延性指如下类型的实例: 对于函数 $f,g:{\prod }_{a:A}B(a)$, $$\mathrm{funExt}:\left(\prod _{a:A}\left({\mathrm{Id}}_{B(a)}(f(a),g(a))\right)\right)\to {\mathrm{Id}}_{{\prod }_{a:A}B(a)}(f,g)$$

以上定义中, 可以将相等类型改为类型论中的值相等, 这种情况下的函数外延性总是成立.

更好的定义

J 公理蕴含 1.1 的逆, 即如下函数:

引理 1.3. 对于函数 $f,g:A\to B$, $$\mathrm{funEx}{\mathrm{t}}^{-1}:\mathrm{Id}(f,g)\to \left(\prod _{a:A}{\mathrm{Id}}_B(f(a),g(a))\right)$$

类似泛等公理的叙述有两种, 我们也可以重新叙述函数外延性, 使得它拥有更好的性质:

定义 1.4. 函数外延性指 1.3 中所述函数是一个等价. 这个说法等价于 1.1. [de Jong 2023]

关于 “等价” 的定义, 参见泛等公理.

2证明

参见: 泛等公理; 立方类型论

•	泛等公理蕴涵函数外延性.
•	区间 (同伦类型论) 的消去规则蕴涵函数的外延性.
•	立方类型论中的区间类型给出了一个函数外延性的证明.
•	外延类型论中能证明函数的外延性.
•	观测类型论中, 函数外延性是函数类型上的相等的定义, 因此不证自明.
•	Martin-Löf 类型论可以基于多项式构造语义, 该语义是函数外延性的反模型. 这也间接说明了函数外延性是独立于 Martin-Löf 类型论的.

3参考文献

•	Tom de Jong (2023). “Domain Theory in Constructive and Predicative Univalent Foundations”. arXiv: 2301.12405. (doi)

术语翻译

函数外延性 • 英文 function extensionality