We propose an enhancement to inductive types and records in a dependent type theory, namely (co)conditions. With a primitive interval type, conditions generalize the cubical syntax of higher inductive types in homotopy type theory, while coconditions generalize the cubical path type. (Co)conditions are also useful without an interval type. The duality between conditions and coconditions is presented in an interesting way: The elimination principles of inductive types with conditions can be internalized with records with coconditions and vice versa. However, we do not develop the metatheory of conditions and coconditions in this paper. Instead, we only present the type checking.

翻译：本文提出一种对依赖类型论中归纳类型与记录类型的增强机制，即(共)条件。在引入原始区间类型的前提下，条件可推广同伦类型论中高阶归纳类型的立方体语法，而共条件则可推广立方体路径类型。即使在没有区间类型的情况下，(共)条件同样具有实用价值。条件与共条件之间的对偶性呈现出一种有趣的对应关系：带条件的归纳类型的消去原理可通过带共条件的记录类型实现内化，反之亦然。然而，本文暂不展开(共)条件的元理论构建，仅着重阐述其类型检查机制。