Compatible squares of functor lenses

References.

• Universal Properties of Proxy Pullbacks (Di Meglio)