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.

翻译：立方类型理论的发展催生了"扩展类型"这一概念，并发现其在同伦类型理论或立方类型理论之外的其他类型理论中也有应用。本文阐述了这些应用，涉及记录类型、元编程、展开控制以及一些更具特异性的场景。