Documentation

Mathlib.CategoryTheory.Bicategory.FunctorBicategory

The bicategory of oplax functors between two bicategories #

Given bicategories B and C, we give a bicategory structure on OplaxFunctor B C whose

Left whiskering of an oplax natural transformation and a modification.

Equations
Instances For

    Right whiskering of an oplax natural transformation and a modification.

    Equations
    Instances For

      A bicategory structure on the oplax functors between bicategories.

      Equations
      • One or more equations did not get rendered due to their size.