Observations relating to the equivalences induced on model sets by bidirectional transformations

Abstract

A bidirectional transformation on a pair of sets of models
induces two principal equivalence relations on each set of
models. Since a model can be uniquely identified by specifying its
equivalence class in each of these relations, they function as a
coordinate system for the model sets, with respect to the
transformation. We prove some results relating to this
observation. Using them we give the implication relationships
between various properties of bidirectional transformations. In
particular, we characterise the bidirectional transformations that
can be decomposed into a pair of lenses working ``tail to tail''.