开放喇叭型理论 (Open Horn Type Theory)

We introduce Open Horn Type Theory (OHTT), an extension of dependent type theory with two primitive judgment forms: coherence and gap, subject to a mutual exclusion law. Unlike classical or intuitionistic negation, gap is not defined via implication but is a primitive witness of non-coherence. Judgments may also be open -- neither coherent nor gapped -- yielding a trichotomy that generalizes the binary derivable/underivable distinction. The central construction is the transport horn: a configuration where a term and a path both cohere, but transport along the path is witnessed as gapped. This captures obstructions that Homotopy Type Theory (HoTT) cannot express, since HoTT's Kan condition guarantees all transport succeeds. We develop the semantics via ruptured simplicial sets -- simplicial sets equipped with coherence and gap structure -- and ruptured Kan complexes, which model types where some horns fill, some are gap-witnessed, and some remain open. We show that HoTT embeds as the coherent fragment of OHTT, recovered by imposing totality. Three classes of obstructions are developed in detail: topological (monodromy, holonomy, characteristic classes), semantic (polysemy, meaning fibrations), and logical (resource-sensitive derivability, substructural failure). In each case, the gap witness is positive structure -- not absence of proof, but certified obstruction.

翻译：我们提出了开放喇叭型理论（OHTT），这是一种对依赖类型理论的扩展，引入了两种基本判断形式：相干性与间隙性，二者受互斥律约束。与经典或直觉主义否定不同，间隙性并非通过蕴含定义，而是非相干性的原始见证。判断也可以是开放的——既不相干也不含间隙——从而形成一种三分法，推广了传统的可推导/不可推导二元区分。核心构造是传输喇叭：一种配置，其中项与路径均保持相干，但沿该路径的传输被见证为含间隙。这捕捉了同伦类型理论（HoTT）无法表达的障碍，因为HoTT的Kan条件保证所有传输均成功。我们通过破裂单纯集——配备相干性与间隙性结构的单纯集——以及破裂Kan复形来发展其语义学，后者用于建模某些喇叭可填充、某些被间隙见证、某些保持开放的类型。我们证明HoTT可嵌入为OHTT的相干片段，通过施加完全性条件恢复。我们详细发展了三类障碍：拓扑类（单值性、和乐性、示性类）、语义类（多义性、意义纤维化）以及逻辑类（资源敏感可推导性、子结构失效）。在每种情形中，间隙见证都是积极结构——并非证明的缺失，而是经过认证的障碍。