Modal dependent type theory and dependent right adjoints

Publikation: Bidrag til tidsskrift/Konferencebidrag i tidsskrift /Bidrag til avisTidsskriftartikelForskningpeer review


  • Lars Birkedal
  • Ranald Clouston, Australian National University
  • ,
  • Bassel Mannaa, EToroX Labs
  • ,
  • Rasmus Ejlers Møgelberg, IT-Universitetet i Kobenhavn
  • ,
  • Andrew M. Pitts, University of Cambridge
  • ,
  • Bas Spitters

In recent years, we have seen several new models of dependent type theory extended with some form of modal necessity operator, including nominal type theory, guarded and clocked type theory and spatial and cohesive type theory. In this paper, we study modal dependent type theory: dependent type theory with an operator satisfying (a dependent version of) the K axiom of modal logic. We investigate both semantics and syntax. For the semantics, we introduce categories with families with a dependent right adjoint (CwDRA) and show that the examples above can be presented as such. Indeed, we show that any category with finite limits and an adjunction of endofunctors give rise to a CwDRA via the local universe construction. For the syntax, we introduce a dependently typed extension of Fitch-style modal λ-calculus, show that it can be interpreted in any CwDRA, and build a term model. We extend the syntax and semantics with universes.

TidsskriftMathematical Structures in Computer Science
Sider (fra-til)118-138
Antal sider21
StatusUdgivet - feb. 2020

Se relationer på Aarhus Universitet Citationsformater

ID: 174760187