A tutorial on implementing De Morgan cubical type theory
Programming Languages
2023-06-07 v4
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.
Cite
@article{arxiv.2210.08232,
title = {A tutorial on implementing De Morgan cubical type theory},
author = {Tesla Zhang},
journal= {arXiv preprint arXiv:2210.08232},
year = {2023}
}
Comments
27 pages