函数外延性

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

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

1定义

参见: 函数类型

简单定义

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

定义 1.1. 函数外延性指如下类型的实例: 对于函数 ,

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

定义 1.2. 函数外延性指如下类型的实例: 对于函数 ,

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

更好的定义

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

引理 1.3. 对于函数 ,

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

定义 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