We consider the equivalence between the two main categorical models for the type-theoretical operation of context comprehension, namely P. Dybjer's categories with families and B. Jacobs' comprehension categories, and generalise it to the non-discrete case. The classical equivalence can be summarised in the slogan: "terms as sections". By recognising "terms as coalgebras", we show how to use the structure-semantics adjunction to prove that a 2-category of comprehension categories is biequivalent to a 2-category of (non-discrete) categories with families. The biequivalence restricts to the classical one proved by Hofmann in the discrete case. It also provides a framework where to compare different morphisms of these structures that have appeared in the literature, varying on the degree of preservation of the relevant structure. We consider in particular morphisms defined by Claraimbault-Dybjer, Jacobs, Larrea, and Uemura.

翻译：我们研究了类型论中上下文理解操作的两种主要范畴模型——即P. Dybjer的带族范畴与B. Jacobs的理解范畴——之间的等价关系，并将其推广至非离散情形。经典等价关系可概括为"项作为截面"这一核心理念。通过确立"项作为余代数"的视角，我们展示了如何利用结构-语义伴随关系证明：理解范畴的2-范畴与（非离散）带族范畴的2-范畴是双等价的。该双等价在离散情形下可约化为Hofmann证明的经典结果。此框架为比较文献中出现的各类结构态射提供了统一基础，这些态射在相关结构的保持程度上存在差异。我们特别考察了由Claraimbault-Dybjer、Jacobs、Larrea和Uemura定义的态射。