This note documents the specification of normal forms in cubical type theory. The definition is already present in the proof of normalization for cubical type theory, but we present it in a more traditional style explicitly for reference.

翻译：本文档记录了立方类型论中范式的规范说明。该定义已蕴含于立方类型论的正规化证明中，但本文以更传统的风格明确呈现，以便于参考。