实现 De Morgan 立方类型论的教程
A tutorial on implementing De Morgan cubical type theory
AI总结：
本文面向具备依赖类型论实现经验者，提供一种实现 De Morgan 立方类型论的教程，涵盖立方体、余纤维化类型检查、传输规则与立方操作，并源自实验系统 Guest0x0。
摘要：
本教程面向已经知道如何实现依赖类型论的读者，解释（一种）实现 De Morgan 立方类型论的方法。内容包括立方体基本概念导引、余纤维化下的类型检查算法、“传输规则”的思想以及立方操作。该教程是名为 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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
