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定义的态射。