Implementation of Two Layers Type Theory in Dedukti and Application to Cubical Type Theory

Bruno Barras
(Inria, Université Paris-Saclay, ENS Paris-Saclay, CNRS, LSV, 91190, Gif-sur-Yvette, France)
Valentin Maestracci
(Université Paris-Saclay, ENS Paris-Saclay, CNRS, LSV, 91190, Gif-sur-Yvette, France)

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öf 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.

In Claudio Sacerdoti Coen and Alwen Tiu: Proceedings Fifteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2020), Paris, France, 29th June 2020, Electronic Proceedings in Theoretical Computer Science 332, pp. 54–67.
Published: 12th January 2021.

ArXived at: https://dx.doi.org/10.4204/EPTCS.332.4 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org