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

1动机

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

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

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

单点,

构造点,

两条线 ,

融贯条件 .

在证明五边形公理的时候, 需要处理形如 这种类型, 用模式匹配处理的话需要考虑 个情况 (我算出来为什么和他幻灯片里面的不一样?), 非常蛋疼.

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

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

2解决方案

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

存在 使得对于任意 , 都有 成立, 其中 带点拓扑空间的类型.

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

引理 2.2. 齐次, 则 齐次.

接下来就是重点了.

可以用缩积–同态伴随 处理成 .

一堆看不懂的操作, 使得可以弄出一个齐次的, 由 构造出来的空间, 使用上面的技巧, 再转换回 .

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