Combinatorial structure of type dependency

TL;DR

This paper explores the combinatorial structure of type dependency in dependent sequent calculi, modeling it via a monad on a presheaf category, revealing connections to decorated ordered trees and well-behaved monads.

Contribution

It provides an explicit categorical framework for understanding type dependency using monads and decorated trees, advancing the mathematical foundation of dependent type theories.

Findings

Type dependency is modeled by a monad on a presheaf category.

The combinatorics are governed by decorated ordered trees.

The monad is a well-behaved local right adjoint.

Abstract

We give an account of the basic combinatorial structure underlying the notion of type dependency. We do so by considering the category of all dependent sequent calculi, and exhibiting it as the category of algebras for a monad on a presheaf category. The objects of the presheaf category encode the basic judgements of a dependent sequent calculus, while the action of the monad encodes the deduction rules; so by giving an explicit description of the monad, we obtain an explicit account of the combinatorics of type dependency. We find that this combinatorics is controlled by a particular kind of decorated ordered tree, familiar from computer science and from innocent game semantics. Furthermore, we find that the monad at issue is of a particularly well-behaved kind: it is local right adjoint in the sense of Street--Weber. In future work, we will use this fact to describe nerves for dependent type theories, and to study the coherence problem for dependent type theory using the tools of two-dimensional monad theory.