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的理解范畴，并将其推广至非离散情形。经典等价可概括为"项作为截面"这一理念。通过将"项视为余代数"，我们展示了如何利用结构-语义伴随关系证明理解范畴的双范畴与（非离散）带族范畴的双范畴是双等价的。该双等价在离散情形下可约化为Hofmann证明的经典结果。该框架为比较文献中出现的、在相关结构保持程度上存在差异的各类态射提供了基础。我们特别考察了由Claraimbault-Dybjer、Jacobs、Larrea和Uemura定义的态射。