更改

#: 即二元态射与“返回函数的一元态射”一一对应。从右向左的逆变换称为'''逆柯里化'''（逆<math>\lambda</math>变换）。

#: 即二元态射与“返回函数的一元态射”一一对应。从右向左的逆变换称为'''逆柯里化'''（逆<math>\lambda</math>变换）。

# '''弱点满射'''：态射 <math>f : A \to Y^A</math> 称为'''弱点满射'''，当且仅当：对任意一元态射 <math>g : A \to Y</math>，都存在点 <math>y : 1 \to A</math>，使得对所有点 <math>a : 1 \to A</math>，都有

# '''弱点满射'''：态射 <math>f : A \to Y^A</math> 称为'''弱点满射'''，当且仅当：对任意一元态射 <math>g : A \to Y</math>，都存在点 <math>y : 1 \to A</math>，使得对所有点 <math>a : 1 \to A</math>，都有

#: <math>\langle a, y \rangle \cdot \bar{f} = a \cdot f</math>

#: <math>\bar{f}(\langle a, y \rangle) = f(a)</math>

#: 其中 <math>\bar{f} : A\times A \to Y</math> 是 <math>g</math> 的逆柯里化。

#: 其中 <math>\bar{f} : A\times A \to Y</math> 是 <math>g</math> 的逆柯里化。

#: 直观含义：所有从 <math>A</math> 到 <math>Y</math> 的一元函数，都可以被 <math>A</math> 中的某个点 <math>y</math> 通过通用二元函数 <math>\bar{f}</math> 表示。

#: 直观含义：所有从 <math>A</math> 到 <math>Y</math> 的一元函数，都可以被 <math>A</math> 中的某个点 <math>y</math> 通过通用二元函数 <math>\bar{f}</math> 表示。

*: <math>g = \delta_A \cdot \bar{f} \cdot \alpha</math>

*: <math>g = \delta_A \cdot \bar{f} \cdot \alpha</math>

*: 对任意点 <math>x : 1 \to A</math>，<math>g</math> 的作用可展开为：

*: 对任意点 <math>x : 1 \to A</math>，<math>g</math> 的作用可展开为：

*: <math>x \cdot g = \alpha\left( \langle x, x \rangle \cdot \bar{f} \right)</math>

*: <math>g(x) = \alpha\left(\bar{f}(\langle x, x \rangle) \right)</math>

*: 其含义是：先将输入 <math>x</math> 复制一份，同时作为 <math>\bar{f}</math> 的两个参数代入（对角线操作），再将计算结果用 <math>\alpha</math> 做变换。这是整个证明的核心——抽象的对角线自指代入。

*: 其含义是：先将输入 <math>x</math> 复制一份，同时作为 <math>\bar{f}</math> 的两个参数代入（对角线操作），再将计算结果用 <math>\alpha</math> 做变换。这是整个证明的核心——抽象的对角线自指代入。

* 步骤3：应用弱点满射条件

* 步骤3：应用弱点满射条件

*: 根据题设，<math>f</math> 是弱点满射。对上述构造的 <math>g : A \to Y</math>，必然存在某个点 <math>y : 1 \to A</math>，使得对所有点 <math>a : 1 \to A</math>，都有：

*: 根据题设，<math>f</math> 是弱点满射。对上述构造的 <math>g : A \to Y</math>，必然存在某个点 <math>y : 1 \to A</math>，使得对所有点 <math>a : 1 \to A</math>，都有：

*: <math>\langle a, y \rangle \cdot \bar{f} = a \cdot g</math>

*: <math>\bar{f}(\langle a, y \rangle) = g(a)</math>

*: 也就是说，<math>y</math> 就是函数 <math>g</math> 对应的“编码”。

*: 也就是说，<math>y</math> 就是函数 <math>g</math> 对应的“编码”。

* 步骤4：对角线代入导出不动点等式

* 步骤4：对角线代入导出不动点等式

*: 将上式中的任意点 <math>a</math> 替换为编码点 <math>y</math> 本身（即将编码代入自身的参数位，完成自指闭合），可得：

*: 将上式中的任意点 <math>a</math> 替换为编码点 <math>y</math> 本身（即将编码代入自身的参数位，完成自指闭合），可得：

*: <math>\langle y, y \rangle \cdot \bar{f} = y \cdot f</math>

*: <math>\bar{f}(\langle y, y \rangle) = f(y)</math>

*: 将右侧的 <math>g</math> 按步骤2的定义展开，代入 <math>y \cdot g = \alpha\left( \langle y, y \rangle \cdot \bar{f} \right)</math>，得到：

*: 将右侧的 <math>g</math> 按步骤2的定义展开，代入 <math>g(y) = \alpha\left(\bar{f}(\langle y, y \rangle) \right)</math>，得到：

*: <math>\langle y, y \rangle \cdot \bar{f} = \alpha\left( \langle y, y \rangle \cdot \bar{f} \right)</math>

*: <math>\bar{f}(\langle y, y \rangle) = \alpha\left(\bar{f}(\langle y, y \rangle) \right)</math>

*: 令 <math>t = \langle y, y \rangle \cdot \bar{f}</math>，这是 <math>Y</math> 的一个点，则上式可写为：

*: 令 <math>t = \langle y, y \rangle \cdot \bar{f}</math>，这是 <math>Y</math> 的一个点，则上式可写为：