Internal split opfibrations, lenses, and decalage

Bryce Clarke – 27 November 2019

In ordinary category theory, split opfibrations are functors equipped with a suitable choice of opcartesian lifts. In this talk, I will show how this elementary definition of a split opfibration may be generalised to the setting of internal category theory. The main result will be to characterise internal split opfibrations as internal lenses which satisfy a property with respect to the decalage comonad.