Open Horn Type Theory

TL;DR

Open Horn Type Theory (OHTT) extends dependent type theory with a novel primitive for non-coherence, enabling the expression of obstructions and gaps in homotopy-theoretic and logical contexts, surpassing HoTT's capabilities.

Contribution

OHTT introduces coherence and gap judgments as primitives, generalizing the binary coherence distinction and capturing obstructions that HoTT cannot express.

Findings

OHTT models obstructions via ruptured simplicial sets.

HoTT embeds as a special case of OHTT.

Three classes of obstructions are formalized: topological, semantic, logical.

Abstract

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.