Comparing Semantic Frameworks for Dependently-Sorted Algebraic Theories
B.P. Ahrens (University of Birmingham, TU Delft - Electrical Engineering, Mathematics and Computer Science)
Peter LeFanu Lumsdaine (Stockholm University)
P.R. North (TU Delft - Electrical Engineering, Mathematics and Computer Science, University of Birmingham, Universiteit Utrecht)
More Info
expand_more
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.
Abstract
Algebraic theories with dependency between sorts form the structural core of Martin-Löf type theory and similar systems. Their denotational semantics are typically studied using categorical techniques; many different categorical structures have been introduced to model them (contextual categories, categories with families, display map categories, etc.) Comparisons of these models are scattered throughout the literature, and a detailed, big-picture analysis of their relationships has been lacking. We aim to provide a clear and comprehensive overview of the relationships between as many such models as possible. Specifically, we take comprehension categories as a unifying language, and show how almost all established notions of model embed as sub-2-categories (usually full) of the 2-category of comprehension categories.