Natural transformations into strict bicategories

Mathlib promotes an ordinary functor into a strict bicategory to a pseudofunctor on the locally discrete source. This module promotes its natural transformations as well.

Main definitions

• CategoryTheory.NatTrans.toStrongTrans promotes a natural transformation to a strong one.

Main results

• CategoryTheory.NatTrans.toStrongTrans_app identifies its component with the original one.

Implementation notes

Strictness turns the coherence maps into equality-induced isomorphisms. The ordinary naturality equality supplies the naturality 2-isomorphism, while the components remain definitionally unchanged.

References

Mathlib's CategoryTheory/Bicategory/Functor/LocallyDiscrete.lean defines CategoryTheory.Functor.toPseudofunctor', the promotion extended here.

Tags

bicategories, locally discrete, natural transformations

def CategoryTheory.NatTrans.toStrongTrans {I : Type u_1} {B : Type u_2} [Category.{v_1, u_1} I] [Bicategory B] [Bicategory.Strict B] {F G : Functor I B} (φ : F ⟶ G) : F.toPseudofunctor'.StrongTrans G.toPseudofunctor'

Promote a natural transformation between ordinary functors into any strict bicategory to a strong transformation of their promoted pseudofunctors. The component at T : LocallyDiscrete I is φ.app T.as by definition.

Equations

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

@[simp]

theorem CategoryTheory.NatTrans.toStrongTrans_app {I : Type u_1} {B : Type u_2} [Category.{v_1, u_1} I] [Bicategory B] [Bicategory.Strict B] {F G : Functor I B} (φ : F ⟶ G) (T : LocallyDiscrete I) : (toStrongTrans φ).app T = φ.app T.as