用户: Ice1000/缩积操作的五边形公理

1动机

缩积操作是 $1$-融贯对称幺半的, 换言之就是它满足五边形公理. 这个性质很有用, 在 Brunerie 数的计算里面, 还有什么上同调谱序列里面也有用到.

但是有一条不成文的规则: 在同伦类型论中, 不论做什么事情, 能不用缩积就尽量不要用. 因为它的消去规则实在是太难对付了.

作为高阶归纳类型, 缩积空间 $A\wedge B$ 由如下构造子生成:

•	单点,
•	从 $A\times B$ 构造点,
•	两条线 ${\mathrm{push}}_l,{\mathrm{push}}_r$,
•	融贯条件 ${\mathrm{push}}_{lr}$.

在证明五边形公理的时候, 需要处理形如 ${\prod }_{x:(A\wedge B)\wedge (C\wedge D)}\to \mathrm{Id}(f(x),g(x))$ 这种类型, 用模式匹配处理的话需要考虑 $4^4$ 个情况 (我算出来为什么和他幻灯片里面的不一样?), 非常蛋疼.

注 1.1 (好消息). 处理这种问题的时候融贯条件是平凡的, 可以作为引理提取.

因此我们现在只需要考虑不含最后一个构造子的情况, 因此减少了一些 (我算的数量又和他不一样, 不写了), 但还是很蛋疼.

2解决方案

定义 2.1. 类型 $A$ 若满足如下条件, 那么它是齐次的:

存在 ${★}_A:A$ 使得对于任意 $a:A$, 都有 $\mathrm{Id}(⟨A,{★}_A⟩,⟨A,a⟩)$ 成立, 其中 $⟨-,-⟩:{\prod }_{A:\mathcal{U}}{\prod }_{a:A}\mathcal{U}$ 是带点拓扑空间的类型.

因此有一个 Evan Cavallo 发明的技巧, 可以对齐次的类型简化这些证明, 简化到只需要考虑前两个构造子 (不需要考虑任何高阶的操作), 但五边形公理里面需要处理的类型不是齐次的. 但有这么个事情.

引理 2.2. 若 $B$ 齐次, 则 $A{\to }_{\ast }B$ 齐次.

接下来就是重点了.

•	可以用缩积–同态伴随将 $(A\wedge B){\to }_{\ast }C$ 处理成 $A{\to }_{\ast }(B{\to }_{\ast }C)$.
•	一堆看不懂的操作, 使得可以弄出一个齐次的, 由 $C$ 构造出来的空间, 使用上面的技巧, 再转换回 $C$.

因此涉及缩积的证明可以基本都化简为关于积 (类型论) 的证明.