The development of cubical type theory inspired the idea of "extension types" which has been found to have applications in other type theories that are unrelated to homotopy type theory or cubical type theory. This article describes these applications, including on records, metaprogramming, controlling unfolding, and some more exotic ones.

翻译：立方类型理论的发展催生了“扩展类型”的概念，该概念已被发现在与同伦类型理论或立方类型理论无关的其他类型理论中具有应用价值。本文描述了这些应用，包括在记录、元编程、展开控制以及一些更具创新性的场景中的应用。