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.

翻译：具有排序间依赖关系的代数理论构成了Martin-Löf类型论及类似系统的结构核心。其指称语义通常借助范畴论技术进行研究；许多不同的范畴结构已被引入以建模这些理论（如上下文范畴、带族范畴、展示映射范畴等）。这些模型之间的比较散见于文献中，至今缺乏对其关系的详细全景式分析。本文旨在为尽可能多的此类模型间关系提供清晰且全面的概述。具体而言，我们以*理解范畴*作为统一语言，并展示几乎所有已建立的模型概念如何嵌入（通常为全嵌入）为理解范畴的2-范畴的子2-范畴。