用户: Ice1000/有向立方类型论

在立方类型论中, 存在区间类型 $\mathbb{I}$, 这是一个双层类型论意义上的 “外类型” (exo-type).

在该区间类型上, 可以定义余纤维化:

•	De Morgan 立方类型论中, 基本的余纤维化有$$\phi ,{\phi }^{\prime }::=\phi \wedge {\phi }^{\prime },\phi \vee {\phi }^{\prime },\neg \phi ,i=1$$这几种, 其中 $i$ 是变量名, 这构成一个 De Morgan 代数. 其它的比如 $i=0$ 可以通过 $\neg (i=1)$ 构造.
•	积立方类型论 (也就是香蕉空间介绍的立方类型论) 中, 有$$\phi ::=\forall i.\phi ,i=j$$这几种 (其中 $i,j$ 可以被特化为 $0$ 或 $1$), $i=j$ 也就是所谓的对角余纤维化.

这些余纤维化表达式有几个名字:

•	公式 (formula)
•	形状 (tope)
•	余纤维化 (cofibration)

所谓有向区间类型 $2$ 是另一个准类型, 构造子和 $\mathbb{I}$ 相同, 但是有不同的余纤维化构造子 (只考虑对积立方类型论的扩展):

$$\phi ::=i=j,i\le j$$

把立方类型论中的区间换成有向区间, 就得到了有向立方类型论 (directed cubical). 将两者结合, 便得到双立方类型论 (bicubical).

显然, 有向区间可以用于描述单形. 考虑如下例子:

$$\{\begin{array}{l}i\le j\mapsto u\end{array}$$

这表示的就是一个三角形, 其上的值是 $u$. 用这个理论可以描述单形, 从而描述一种 $\infty$-范畴的模型 (Riehl–Shulman, 单类型论).