A Judgmental Construction of Directed Type Theory

TL;DR

This paper reformulates directed type theory using a logical calculus with multiple context zones, introducing neutral and polar variables, and develops categorical semantics for dual-context systems, especially in the setting of synthetic preorders.

Contribution

It presents a novel logical calculus for directed type theory with multiple contexts and dual variables, and introduces dual CwF for categorical semantics.

Findings

Logical calculus with multiple context zones for directed type theory.

Introduction of neutral and polar variables with different functoriality.

Development of dual CwF as a categorical semantics framework.

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.