Semantics for two-dimensional type theory

Benedikt Ahrens, Paige Randall North, Niels van der Weide

Research output: Working paperPreprintAcademic

Abstract

We propose a general notion of model for two-dimensional type theory, in the form of comprehension bicategories. Examples of comprehension bicategories are plentiful; they include interpretations of directed type theory previously studied in the literature. From comprehension bicategories, we extract a core syntax, that is, judgment forms and structural inference rules, for a two-dimensional type theory. We prove soundness of the rules by giving an interpretation in any comprehension bicategory. The semantic aspects of our work are fully checked in the Coq proof assistant, based on the UniMath library. This work is the first step towards a theory of syntax and semantics for higher-dimensional directed type theory.
Original languageEnglish
PublisherarXiv
DOIs
Publication statusPublished - 25 Jan 2022

Bibliographical note

v2: final version for LICS 2022. v3: long version - for detailed log, see Section 1.5 Version History

Keywords

  • cs.LO
  • math.CT

Fingerprint

Dive into the research topics of 'Semantics for two-dimensional type theory'. Together they form a unique fingerprint.

Cite this