The Internal Language of Comprehension Categories

Master thesis (2024)

Authors

N. Najmaei Electrical Engineering, Mathematics and Computer Science

Contributors

B.P. Ahrens Programming Languages - EEMCS (mentor)
K.F. Wullaert Programming Languages - EEMCS (graduation committee member)
N. Yorke-Smith Algorithmics - EEMCS (graduation committee member)
Faculty
Electrical Engineering, Mathematics and Computer Science
More Info
expand_more

Published Date

27-08-2024

Language

English

Reuse Rights

Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.

Faculty

Electrical Engineering, Mathematics and Computer Science

Abstract

Denotational semantics of type theories provide a framework for understanding and reasoning about type theories and the behaviour of programs and proofs. In particular, it is important to study what can and can not be proved within Martin-Löf Type Theory (MLTT) as it is the basis of proof assistants like Agda, Lean and Coq. Many models, including a certain class of comprehension categories, full and split comprehension categories, have been studied for the semantics of dependent type theories. The motivation for this work comes from the fact that not all comprehension categories are full and split, and one expects that type theories more general than MLTT can be interpreted in a comprehension category which is not full and split.

In this thesis, we first study how MLTT is interpreted in full split comprehension categories through concrete examples. Next, we investigate type theories that can be interpreted in comprehension cat- egories which are not necessarily full and split. For this, we propose a candidate type theory for the internal language of comprehension categories by extracting a type theory from the semantics given by a general comprehension category which is not full and split. We also give an interpretation of this type theory in every comprehension category.