  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.
