DOI: 10.1017/s0960129526100565 ISSN: 0960-1295
Reflexive graph lenses in univalent foundations
Jonathan Sterling Abstract
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
left parenthesis equals Subscript upper A Baseline comma bold r bold e bold f bold l right parenthesis
(
=
A
,
r
e
f
l
)
$(=_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 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.