Martin-Löf's identity types provide a generic (albeit opaque) notion of identification or "equality" between any two elements of the same type, embodied in a canonical reflexive graph structure $(=_A, \mathbf{refl})$ on any type $A$. The miracle of Voevodsky's univalence principle is that it ensures, for essentially any naturally occurring structure in mathematics, that this the resultant notion of identification is equivalent to the type of isomorphisms in the category of such structures. Characterisations of this kind are not automatic and must be established one-by-one; to this end, several authors have employed reflexive graphs and displayed reflexive graphs to organise the characterisation of identity types. We contribute reflexive graph lenses, a new family of intermediate abstractions lying between families of reflexive graphs and displayed reflexive graphs that simplifies the characterisation of identity types for complex structures. Every reflexive graph lens gives rise to a (more complicated) displayed reflexive graph, and our experience suggests that many naturally occurring displayed reflexive graphs arise in this way. Evidence for the utility of reflexive graph lenses is given by means of several case studies, including the theory of reflexive graphs itself as well as that of polynomial type operators. Finally, we exhibit an equivalence between the type of reflexive graph fibrations and the type of univalent reflexive graph lenses.

翻译：马丁-洛夫恒等类型为同一类型中任意两个元素间的同一性或"相等性"提供了通用（尽管不透明）的概念，具体体现在任意类型A上规范的自反图结构$(=_A, \mathbf{refl})$中。Voevodsky单值原理的非凡之处在于，它确保对于数学中几乎所有自然出现的结构，这种恒等概念等价于此类结构范畴中同构的类型。这类刻画并非自动成立，必须逐一验证；为此，多位学者采用自反图与展示自反图来组织恒等类型的刻画工作。我们提出自反图透镜这一新型中间抽象族，它介于自反图族与展示自反图之间，能够简化复杂结构的恒等类型刻画。每个自反图透镜都会导出（更复杂的）展示自反图，而我们的经验表明许多自然出现的展示自反图正是由此产生。通过多项案例研究（包括自反图理论本身及多项式类型算子理论）证明了自反图透镜的实用性。最后，我们展示了自反图纤维化类型与单值自反图透镜类型之间的等价性。