Symmetric lenses as Mealy morphisms

Bryce Clarke – 21 August 2019

Lenses were originally introduced as a mathematical structure which captures the notion of synchronisation between a pair of sets. When extending this idea to consider synchronisation between a pair of categories, we obtain functors akin to split Grothendieck opfibrations lacking the universal property. Internal lenses have previously been introduced to describe synchronisation between internal categories. The purpose of this talk is to motivate the definition of a symmetric lens between internal categories as a pair of internal Mealy morphisms (or two-dimensional partial maps) and establish the relationship with spans of internal lenses, generalising previous work of Johnson and Rosebrugh.