A Judgmental Construction of Directed Type Theory

TL;DR

This work develops a judgmental directed type theory with dual-context semantics, introducing neutral and polarized variables and a polarity calculus to block symmetry in directed identity types. It furnishes syntax for two-zone contexts, core and opposite type directions, and a bidirectional Hom type with a unified $\mathsf{J}^{\pm}$ rule, along with coercions that connect zones. Semantically, it presents a groupoid-category (and setoid-preorder) model and proposes an abstract dual CwF framework to support general models of dual-context theories. An application to synthetic rewriting systems demonstrates how directed reduction can be internalized and manipulated within the theory, distinguishing core equality from extensional equivalence and setting the stage for future explorations of higher-dimensionalDirected type theories and their model theory.

Abstract

We reformulate recent advances in directed type theory--a type theory where the types have the structure of synthetic (higher) categories--as a logical calculus with multiple context 'zones', following the example of Pfenning and Davies. This allows us to have two kinds of variables--'neutral' and 'polar'--with different functoriality requirements. We focus on the lowest-dimension version of this theory (where types are synthetic preorders) and apply the logical language to articulate concepts from the theory of rewriting. We also take the occasion to develop the categorical semantics of dual-context systems, proposing a notion of dual CwF to serve as a common structural base for the model theories of such logics.

Figures (6)

• Figure 2.1: Basic rules of the polarity calculus
• Figure 2.2: Rules for core types.
• Figure 2.3: Rules for hom-types.
• Figure 2.4: Restriction to synthetic (0,1)-categories
• Figure 2.5: Rules for opposite and core hom-terms. For the coercions of $x$ in Core Hom, note that we use Core Negation to view $x$ as a term of type $(A^-)^\flat$. So then $\langle+\rangle x\colon A^-$ and $\langle-\rangle x\colon (A^-)^-$, i.e. $A$.

Theorems & Definitions (6)

• Definition 2.1
• Definition 3.1
• Definition 3.2
• Definition 3.3
• Definition 3.4
• Definition 3.5