| Title: |
From Semantics to Syntax: A Type Theory for Comprehension Categories |
| Authors: |
Najmaei, Niyousha; Van der Weide, Niels; Ahrens, Benedikt; North, Paige Randall; Sub Software Technology; Sub Fundamental Mathematics |
| Publication Year: |
2026 |
| Subject Terms: |
categorical semantics; comprehension categories; subtyping; type theory; Software; Safety; Risk; Reliability and Quality |
| Description: |
Recent models of intensional type theory have been constructed in algebraic weak factorization systems (AWFSs). AWFSs give rise to comprehension categories that feature non-trivial morphisms between types; these morphisms are not used in the standard interpretation of Martin-Löf type theory in comprehension categories. We develop a type theory that internalizes morphisms between types, reflecting this semantic feature back into syntax. Our type theory comes with Π-, Σ-, and identity types. We discuss how it can be viewed as an extension of Martin-Löf type theory with coercive subtyping, as sketched by Coraglia and Emmenegger. We furthermore define semantic structure that interprets our type theory and prove a soundness result. Finally, we exhibit many examples of the semantic structure, yielding a plethora of interpretations. |
| Document Type: |
article in journal/newspaper |
| File Description: |
application/pdf |
| Language: |
English |
| ISSN: |
2475-1421 |
| Relation: |
https://dspace.library.uu.nl/handle/1874/480511 |
| Availability: |
https://dspace.library.uu.nl/handle/1874/480511 |
| Rights: |
info:eu-repo/semantics/OpenAccess |
| Accession Number: |
edsbas.61EEE49F |
| Database: |
BASE |