Implementation of Two Layers Type Theory in Dedukti and Application to Cubical Type Theory
Logic in Computer Science
2021-01-12 v1
Abstract
In this paper, we make a substantial step towards an encoding of Cubical Type Theory (CTT) in the Dedukti logical framework. Type-checking CTT expressions features a decision procedure in a de Morgan algebra that so far could not be expressed by the rewrite rules of Dedukti. As an alternative, 2 Layer Type Theories are variants of Martin-L\"of Type Theory where all or part of the definitional equality can be represented in terms of a so-called external equality. We propose to split the encoding by giving an encoding of 2 Layer Type Theories (2LTT) in Dedukti, and a partial encoding of CTT in 2LTT.
Keywords
Cite
@article{arxiv.2101.03810,
title = {Implementation of Two Layers Type Theory in Dedukti and Application to Cubical Type Theory},
author = {Bruno Barras and Valentin Maestracci},
journal= {arXiv preprint arXiv:2101.03810},
year = {2021}
}
Comments
In Proceedings LFMTP 2020, arXiv:2101.02835