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

TL;DR

This paper advances the encoding of Cubical Type Theory in Dedukti by introducing a two-layer type theory approach, enabling better representation of definitional equality and facilitating the implementation of CTT within a logical framework.

Contribution

It proposes a novel encoding of two-layer type theories in Dedukti and a partial encoding of Cubical Type Theory, addressing previous limitations in representing definitional equality.

Findings

Successful encoding of 2 Layer Type Theories in Dedukti

Partial encoding of Cubical Type Theory in 2LTT

Enhanced decision procedures for type-checking in the framework

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.