Modifications between transformations of pseudofunctors

In this file we define modifications of strong transformations of pseudofunctors. They are defined similarly to modifications of transformations of oplax functors.

Main definitions

Given two pseudofunctors F and G, we define:

• Pseudofunctor.StrongTrans.Modification η θ : modifications between strong transformations η and θ (between F and G).
• Pseudofunctor.StrongTrans.homCategory F G : the category structure on strong transformations between F and G, where the morphisms are modifications, and composition is given by vertical composition of modifications. Note that this a scoped instance in the Pseudofunctor.StrongTrans namespace, so you need to run open scoped Pseudofunctor.StrongTrans to access it.