Dinaturality for Double Categories

TL;DR

This paper extends dinaturality to double categories, introducing dinatural transformations and modifications, and explores their algebraic properties and diagrammatic calculus, with applications to Eilenberg-Kelly graphs and adjunction laws.

Contribution

It introduces dinatural transformations for double categories and analyzes their composition and algebraic structure, extending existing categorical concepts.

Findings

Dinatural transformations do not generally compose with each other.

Dinatural transformations compose with natural transformations.

Application to Eilenberg-Kelly graphs and adjunction laws.

Abstract

In this paper we extend the concept of dinaturality to the setting of double categories. We introduce the dinatural versions of double-categorical transformations and modifications, and show that ordinary natural transformations and modifications correspond to dinatural ones between dummy functors. Although dinatural transformations don't generally compose with each other, they do compose with natural transformations, and we investigate the algebra of this composition. In our motivating example of dinaturality for double categories, we derive the caps and cups of Eilenberg-Kelly graphs for extranatural transformations as dinatural transformation components, and the corresponding adjunction laws as (di)modification components. In an appendix we extend the surface diagram calculus for the locally cubical Gray category of small double categories to include dinatural constructions.