Diagram chasing with the mates correspondence

Emily Riehl – 1 February 2023

This talk describes a proof technique used in recent joint work with Sina Hazratpour (https://arxiv.org/abs/2210.00078) to prove that certain diagrams of natural transformations between composite functors between the slices of a locally cartesian closed category commute. We show that all of the natural transformations in our diagrams arise by iteratively taking mates of identity natural transformations. We then iteratively apply the double functoriality of the mates correspondence --- a classical theorem of Kelly and Street --- to reduce our pasted composites of mates to pasted composites of identity natural transformations, which self-evidently commute.