A translation of Cubical Type Theory in lambdapi.
This uses a Two-level Type Theory, with the external layer containing the interval type, face lattice and an equality representing the cubical conversion over the internal layer, as the latter is too expressive to be encoded with Dedukti rewrite rules.
This is based on previous work avaliable here : https://github.com/vmaestracci/CTTDedukti.