Definition. Total Bicategory

The total bicategory of a displayed bicategory over 𝒦︀ packages the base and the displayed data together, one dimension up from the total category of a displayed category.

  • Its 0-cells are pairs of a 0-cell of 𝒦︀ and a displayed 0-cell over it.
  • Its hom-category from to is the total category of the displayed hom-category . So a 1-cell is a pair and a 2-cell is a pair .
  • Identities, composition, unitors and associator are pairs of the base structure and the displayed structure over it, and the triangle and pentagon hold because they hold in the base and, over that, in the displayed bicategory.

Projecting to first components is a pseudofunctor whose unit and composition comparisons are identity 2-cells.

total-bicategory definition entries/bicategory/total-bicategory.hel