Definition. The Bicategory of Categories

The bicategory of categories 𝖢𝖠𝖳 has

  • as 0-cells, categories (at a fixed pair of universe levels, for objects and for morphisms);
  • as hom-category 𝖢𝖠𝖳(𝒞︀,𝒟︀), the functor category [𝒞︀,𝒟︀], so 1-cells are functors and 2-cells are natural transformations;
  • as identity 1-cell, the identity functor;
  • as composition, 𝐹⋆𝐺=𝐺∘𝐹 on functors. On natural transformations 𝛽:𝐹⇒𝐹′ and 𝛾:𝐺⇒𝐺′ the horizontal composite is given directly by its components

    (𝛽⋆𝛾)𝑐=𝐺(𝛽𝑐)⋆𝛾𝐹′𝑐.

Every component of the left unitor, the right unitor and the associator is an identity morphism, and their inverses are identities too. So the only content of the triangle and pentagon is that composites of identities are identities.

𝖢𝖠𝖳 is still a bicategory and not a strict 2-category: Id∘𝐹 and 𝐹 agree on objects and on morphisms, but in the formalization they are not the same functor definitionally. The structure cells are there to name that agreement.

A monad in 𝖢𝖠𝖳 is an ordinary monad on a category, and a prestack is a pseudofunctor into 𝖢𝖠𝖳.

bicategory-of-categories definition entries/bicategory/bicategory-of-categories.hel