同伦类型论里面 Univance Axiom 以 Axiom 的形式存在，不符合构造主义的追求，立方类型论通过一个很神奇的方法解决了这个问题：直接把「路径」看成「函数」。但在看成函数之后如何保持路径本身应有的性质、在 Martin-Löf 类型论的基础上修改或添加了什么规则、能够实现什么有趣的事情、在软件工程的模型中对应什么，则是本次博客需要探索的问题。
路径的性质
Cubical Agda 的原论文先介绍了他们的 ua 函数是可计算的（但没有讲具体是怎么实现的），然后引出了 dependent path 和 nondependent path, 分别对应 heterogeneous 和 homogeneous 的情况，同时可以看出 Agda 里面用 l 指定 universe level, 疑似用 Set l 代表正常意义上的 Type 或者 U.
这样，路径的形成规则便是 PathP : (A : I -> Set l) -> A i0 -> A i1 -> Set l, 也可以视为 Set l 的一条引入规则。由于把路径定义成函数，路径的其余四条规则都比较好处理，例如对于非 HIT (Higher Inductive Types, not Harbin Institute of Technology) 的引入规则 refl 则可以被定义出来，refl : \i => x.
在讲涉及消去规则的 transp 的时候感觉有点模糊的地方，暂时放着。例如，论文前面说 transp 的用法是 transp (λ i → p i) i0 a, 但后面又出现了 transp A r a, A 是一个类型而 (λ i → p i) 是一个函数，感觉有点奇怪。论文后面用 transp 构造出 transport 和 subst, 可以认为是路径消去规则的几种不同理解方式。同时，transp 的纯构造定义论文暂时也没有讲。
能实现的事情
利用可计算的 transport 函数可以实现把我们认为比较直观的「等价关系」投射到 Agda 这种定理证明验证器中，例如可以利用这个特性在证明中结合自然数的一进制和二进制表示方式，在涉及大数计算的时候用二进制，涉及递推的时候使用一进制（当然因为证明本身是模块化的就显然可以这样做），同时规避二进制规则复杂和一进制计算效率低的缺点。
同时上述思路对其他 inductive types, coinductive types 和 higher inductive types 也适用，虽然我感觉 coinductive types 就是允许懒求值的 inductive types, 这样可以搞一些无穷长的变量。在 higher inductive types 里面，虽然 path 本身不是值，但是由于其可以被视为 I 到值的函数，定义的时候直接使用类似于 cons (p i) = … 的形式即可。
自然地，可以利用 CuTT 实现对代数拓扑的内容进行建模。在甜甜圈的定义上，HoTT 采用了 base, l1, l2, sphere : l1+l2=l2+l1 的定义，而 CuTT 采用了 base, l1, l2, square : PathP (λ i → l1 i ≡ l1 i) l2 l2 的定义，或许更适合用于推理一些，同时也更方便理解为什么这玩意会形成甜甜圈。理解的关键在于先把无论它形成什么妖魔鬼怪展开，注意展开和收回去都会保持拓扑的性质，这样容易发现 square 会形成一个对边需要重合的方形，收回去的时候就变成甜甜圈了。通过计算可以很容易发现甜甜圈和两个圈的笛卡儿积等价。
调整的规则
似乎 Path 的单点固定消去规则是可以证明的，但是 for details see the lecture notes or the paper.
在 ctt 的 blog 里面出现了不知道怎么定义的 comp, 又阻碍了我理解 path 的消去规则的实现，悲。5:05 PM, 先去吃饭力！
我的评价是，要理解 CuTT 可以从 ctt 的 haskell 源码开始，这玩意似乎包含了整个 parser 和 typecheck，好像就一两千行，比较符合我梦想中的样子。
在暑校群里看到一个中文 CuTT 讲义，我打算先看下这个讲义能不能解决我的问题，不过 ctt 的源码还是想看。
在软件工程模型对应的东西
根据我一天的思考，这玩意对应的「等价关系」能够解决很多细微的问题。
例如，之前一直感觉束手无策的「逻辑和算法优化解耦」，似乎使用等价关系就能实现，参考一进制和二进制转换的例子，这样可以把常用的算法建模起来，但在实际使用的时候选择天真的数据结构。
不过如果目标只是「实现一个功能」，似乎不会出现相等的类型，便在这方面用不上 CuTT 了。但使用 CuTT 可以方便证明程序中存在的一些性质，不过我感觉不是特别重要。
或许这玩意的优势正在于构建人的思维模式和计算机思维模式之间的「同伦桥梁」，如果只求架构的话自然不需要 CuTT, 但往往在现实问题中有些天真的算法会过于缓慢，换言之使用 CuTT 允许我们使用比现有习惯「更」天真的数据结构，而不仅是节约一些极端的性能优化时间。CuTT 或将允许我们「完全」使用符合人类思维方式的思路进行顶层逻辑设计，让 AI 负责优化底层算法（或许能够把 AI 里面的思路提取出来然后造出更逆天的 AI！）
更难的理论往往能让事情更简单，以退为进，或许 CuTT 就是个好的例子。
总结
前面的 CuTT 以后再来探索吧！