用户: 幂零几何/单纯类型论的另一种方案

在 Riehl–Shulman 2017 中, 作者为了合法地让态射类型的两端以判断意义的相等固定住, 而引入了分为 cube, tope ,type 三层的分层类型论. 这么做虽然看起来方便了, 但是又产生了新的 bug, 比如说在 cube 和 tope 层无法量化自然数 $\mathbb{N}$, 因此无法递归地定义和研究 n-单形 ${\Delta }^n$. 如果试图引入补丁来修复这个问题的话, 只会把史山越堆越大.

另一方面, 把判断意义相等放宽为命题意义相等带来的麻烦也并没有作者所想象的那么大, 因为对于所关心的问题来说, 相等类型所带来的信息都是可缩的, 本质上并没有额外的资料需要处理.

因此, 这里尝试使用更基础的单层类型论的方式 (类似 Gratzer-Weinberger-Buchholtz 2024 所说的那样), 重写文中所用到的一些基本概念与定理.

内容未经校对, 仅供参考.

1单纯形

公理 1.1. 单纯类型论中有一个有向区间类型 $2:\mathrm{Set}$, 是一个有界全序集, 即给定 $2$ 中元素: $$0:21:2$$且对任意的 $x,y,z:2$, 有: $$\begin{array}{rl}x\le y& :\mathrm{Prop}\\ {\mathrm{ordrefl}}_x& :x\le x\\ {\mathrm{ordtrans}}_{x,y,z}& :(x\le y)\times (y\le z)\to (x\le z)\\ {\mathrm{ordantisym}}_{x,y}& :(x\le y)\times (y\le x)\to (x=y)\\ {\mathrm{ordtot}}_{x,y}& :1\to \Vert (x\le y)+(y\le x)\Vert \\ {\mathrm{ordlow}}_x& :0\le x\\ {\mathrm{ordup}}_x& :x\le 1\\ \mathrm{ordnontriv}& :\neg (0=1)\end{array}$$注意这些资料中没有取否操作, 因此不能构造出 $2$ 到自身交换 0 和 1 的函数, 确保了有向性.

实际上, 有了全序结构就可以定义析取 (较大值) 和合取 (较小值) 运算, 为此需要用到一个比较实用的引理.

引理 1.2. 对于纯命题 $A,B:\mathrm{Prop}$, 有如下推出方块: $$A\times BAB\Vert A+B\Vert {\mathrm{pr}}_1{\mathrm{pr}}_2┘|\mathrm{inl}||\mathrm{inr}|$$

证明. (...)

$\square$

推论 1.3. $$\frac{\begin{array}{c}a⊢A:\mathrm{Prop}\Gamma ⊢B:\mathrm{Prop}\Gamma ⊢C:\mathcal{U}\\ \Gamma ,a:A⊢c_1(a):C\Gamma ,b:B⊢c_2(b):C\\ \Gamma ⊢\mathrm{cons}:\prod _{x:A\times B}{c}_1({\mathrm{pr}}_1(x))=c_2({\mathrm{pr}}_2(x))\end{array}}{\Gamma ,\Vert A+B\Vert ⊢{\mathrm{cases}}^{A,B}(c_1,c_2):C}$$用人话说就是, 在 $A$ 的前提下给定 $c_1\in C$, 在 $B$ 的前提下给定 $c_2\in C$, 并且两者在 $A\times B$ (即 $A$ 且 $B$) 时相等, 那么在 $\Vert A+B\Vert$ (即 $A$ 或 $B$) 的前提下可以给出 ${\mathrm{cases}}^{A,B}(c_1,c_2):C$. 这也是个经典的结论.

同样的结论也可以推广到 $n$ 个命题的情况.

定义 1.4. 对 $x,y:2$, 定义析取运算 $\vee \vee$ 与合取运算 $\wedge \wedge$ 为$$\begin{gathered} x\vee \vee y:\equiv {\mathrm{cases}}^{x\le y,y\le x}(y,x) \\ x\wedge \wedge y:\equiv {\mathrm{cases}}^{x\le y,y\le x}(x,y) \end{gathered}$$

以有向区间为基础可以定义单形的概念.

定义 1.5. 定义 $\mathbf{n}$-单形 ${\Delta }^n$ 为: $${\Delta }^n:\equiv \{(t_1,\cdots ,t_n):2^n|t_n\le \cdots \le t_1\}$$

(...)

2相对依值函数

定义 2.1. 令 $B:A\to \mathcal{U},\varphi :A\to \mathrm{Prop}$, 引入如下关于子类型的简写: $$A|\varphi :\equiv \sum _{a:A}\varphi (a),b:\prod _{a:A|\varphi }B(a)$$上式中最后的 $B(a)$ 中的 $a$ 是 $i_{\varphi }(a)$ 的简写, 其中 $i_{\varphi }:A|\varphi \hookrightarrow A$ 为子类型的嵌入.

定义相对依值函数类型为: $$⟨\prod _{a:A}B(a){|}_b^{\varphi }⟩:\equiv \sum _{f:{\prod }_{a:A}B}\prod _{a:A|\varphi }(f(a)=b(a))$$说人话就是, ${\prod }_{a:A}B(a)$ 当中在子类型 $A|\varphi$ 上固定为 $b(a)$ 的那些函数.

类似于普通的依值函数类型, 对于 $B$ 不依赖于 $a$ 的情况, 我们将其写成 $⟨A\to B{|}_b^{\varphi }⟩$.

出于记号的灵活性, 书写时上式中的 $\varphi$ 有时也会用 $A|\varphi$ 代替, 如 $⟨A\to B{|}_b^{A|\varphi }⟩$.

(...)

定义 2.2. 对 $x,y\in A$, 定义态射类型为: $${\mathrm{hom}}_A(x,y):\equiv ⟨{\Delta }^1\to A{|}_{[x,y]}^{\partial {\Delta }^1}⟩$$

(...)