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

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

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

De Morgan 立方类型论中, 基本的余纤维化有这几种, 其中 是变量名, 这构成一个 De Morgan 代数. 其它的比如 可以通过 构造.

积立方类型论 (也就是香蕉空间介绍的立方类型论) 中, 有这几种 (其中 可以被特化为 ), 也就是所谓的对角余纤维化.

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

公式 (formula)

形状 (tope)

余纤维化 (cofibration)

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

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

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

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