Combinatorial structure of type dependency

Richard Garner*

*Corresponding author for this work

    Research output: Contribution to journalArticle

    1 Citation (Scopus)

    Abstract

    We give an account of the basic combinatorial structure underlying the notion of type dependency. We do so by considering the category of generalised algebraic theories in the sense of Cartmell, 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.

    Original languageEnglish
    Pages (from-to)1885-1914
    Number of pages30
    JournalJournal of Pure and Applied Algebra
    Volume219
    Issue number6
    DOIs
    Publication statusPublished - 1 Jun 2015

    Fingerprint Dive into the research topics of 'Combinatorial structure of type dependency'. Together they form a unique fingerprint.

    Cite this