Semantics for two-dimensional type theory

Benedikt Ahrens, Paige Randall North, Niels van der Weide

Research output: Chapter in Book/Conference proceedings/Edited volumeConference contributionScientificpeer-review

3 Citations (Scopus)
63 Downloads (Pure)


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
Title of host publicationProceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2022
Place of PublicationNew York
PublisherAssociation for Computing Machinery (ACM)
Number of pages14
ISBN (Print)978-1-4503-9351-5
Publication statusPublished - 2022
Event37th Annual ACM/IEEE Symposium
on Logic in Computer Science
- Haifa, Israel
Duration: 2 Aug 20225 Aug 2022
Conference number: 27


Conference37th Annual ACM/IEEE Symposium
on Logic in Computer Science
Abbreviated titleLICS ’22


  • directed type theory
  • dependent types
  • comprehension bicategory,
  • computer-checked proof


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

Cite this