论文标题
关于实施De Morgan立方体理论的教程
A tutorial on implementing De Morgan cubical type theory
论文作者
论文摘要
该教程向知道如何实施依赖类型理论的人解释了如何实施De Morgan Cubty类型理论。它包含对立方体的基本概念的介绍，类型检查算法在联合启用下，“运输规则”和立方体操作的想法。本教程是立方体理论实验实现的副产品，称为Guest0x0。
This tutorial explains (one way) how to implement De Morgan cubical type theory to people who know how to implement a dependent type theory. It contains an introduction to basic concepts of cubes, type checking algorithms under a cofibration, the idea of "transportation rules" and cubical operations. This tutorial is a by-product of an experimental implementation of cubical type theory, called Guest0x0.
