更改

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

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

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

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

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

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

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

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

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

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

 

任取 <math>Y</math> 上的自态射 <math>t : Y \to Y</math>，我们通过构造得到它的不动点，步骤如下：

任取 <math>Y</math> 上的自态射 <math>t : Y \to Y</math>，我们通过构造得到它的不动点，步骤如下：

* 步骤1：逆柯里化得到通用二元态射

* 步骤1：逆柯里化得到通用二元态射

根据指数伴随的柯里化同构，态射 <math>g : A \to Y^A</math> 唯一对应一个二元态射 <math>\bar{g} : A \times A \to Y</math>（称为 <math>g</math> 的逆柯里化），满足：

*: 根据指数伴随的柯里化同构，态射 <math>g : A \to Y^A</math> 唯一对应一个二元态射 <math>\bar{g} : A \times A \to Y</math>（称为 <math>g</math> 的逆柯里化），满足：

:<math>\bar{g} = (A \times g) \cdot \epsilon_A</math>

*: <math>\bar{g} = (A \times g) \cdot \epsilon_A</math>

其中 <math>A \times g</math> 是积函子作用在态射 <math>g</math> 上的结果。

*: 其中 <math>A \times g</math> 是积函子作用在态射 <math>g</math> 上的结果。

直观上，<math>\bar{g}</math> 是范畴内部的“通用解释器”：第一个参数是输入值，第二个参数是函数的编码，输出函数作用在输入上的结果。

*: 直观上，<math>\bar{g}</math> 是范畴内部的“通用解释器”：第一个参数是输入值，第二个参数是函数的编码，输出函数作用在输入上的结果。

* 步骤2：构造对角线复合函数

* 步骤2：构造对角线复合函数

取对角态射 <math>\delta_A : A \to A \times A</math>，将其与 <math>\bar{g}</math>、<math>t</math> 依次复合，得到一元态射 <math>f : A \to Y</math>：

*: 取对角态射 <math>\delta_A : A \to A \times A</math>，将其与 <math>\bar{g}</math>、<math>t</math> 依次复合，得到一元态射 <math>f : A \to Y</math>：

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

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

 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

:<math>\langle y, y \rangle \cdot \bar{g} = t\left( \langle y, y \rangle \cdot \bar{g} \right)</math>

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

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

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

:<math>z = z \cdot t</math>

*: <math>z = z \cdot t</math>

* 步骤5：结论

* 步骤5：结论

点 <math>z</math> 满足自态射 <math>t</math> 的不动点定义。由于 <math>t</math> 是任意选取的自态射，因此对象 <math>Y</math> 具有不动点性质。

*: 点 <math>z</math> 满足自态射 <math>t</math> 的不动点定义。由于 <math>t</math> 是任意选取的自态射，因此对象 <math>Y</math> 具有不动点性质。

证毕。

证毕。