Symmetric lenses as Mealy morphisms (part 2)

Bryce Clarke – 25 September 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. Continuing from Part I on 24 August, the purpose of this talk is to motivate the definition of a symmetric lens between internal categories as a pair of internal Mealy morphisms and establish the relationship with spans of internal lenses, generalising previous work of Johnson and Rosebrugh.