A tutorial on implementing De Morgan cubical type theory

TL;DR

This tutorial guides implementers on how to realize De Morgan cubical type theory, covering core concepts, algorithms, and operations, based on an experimental implementation called Guest0x0.

Contribution

It provides a detailed, practical tutorial on implementing De Morgan cubical type theory for those familiar with dependent type theory.

Findings

Developed an implementation called Guest0x0

Clarified core concepts and algorithms for cubical type theory

Demonstrated practical application through an experimental implementation

Abstract

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.