Documentation

Mathlib.CategoryTheory.Bicategory.Product

Cartesian products of bicategories #

We define the bicategory instance on B × C when B and C are bicategories.

We define:

source
@[instance_reducible]
instance CategoryTheory.Bicategory.prod (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] :
Bicategory (B × C)

The cartesian product of two bicategories.

Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem CategoryTheory.Bicategory.prod_homCategory_comp_fst (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] (X Y : B × C) {X✝ Y✝ Z✝ : (X.1 ⟶ Y.1) × (X.2 ⟶ Y.2)} (f : (X✝.1 ⟶ Y✝.1) × (X✝.2 ⟶ Y✝.2)) (g : (Y✝.1 ⟶ Z✝.1) × (Y✝.2 ⟶ Z✝.2)) :
(CategoryStruct.comp f g).1 = CategoryStruct.comp f.1 g.1
source
@[simp]
theorem CategoryTheory.Bicategory.prod_homCategory_id_fst (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] (X Y : B × C) (X✝ : (X.1 ⟶ Y.1) × (X.2 ⟶ Y.2)) :
(CategoryStruct.id X✝).1 = CategoryStruct.id X✝.1
source
@[simp]
theorem CategoryTheory.Bicategory.prod_leftUnitor_inv_fst (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {a✝ b✝ : B × C} (f : a✝ ⟶ b✝) :
(leftUnitor f).inv.1 = (leftUnitor f.1).inv
source
@[simp]
theorem CategoryTheory.Bicategory.prod_associator_hom_snd (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {a✝ b✝ c✝ d✝ : B × C} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) (h : c✝ ⟶ d✝) :
(associator f g h).hom.2 = (associator f.2 g.2 h.2).hom
source
@[simp]
theorem CategoryTheory.Bicategory.prod_homCategory_id_snd (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] (X Y : B × C) (X✝ : (X.1 ⟶ Y.1) × (X.2 ⟶ Y.2)) :
(CategoryStruct.id X✝).2 = CategoryStruct.id X✝.2
source
@[simp]
theorem CategoryTheory.Bicategory.prod_whiskerRight_fst (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {a✝ b✝ c✝ : B × C} {f✝ g✝ : a✝ ⟶ b✝} (θ : f✝ ⟶ g✝) (g : b✝ ⟶ c✝) :
(whiskerRight θ g).1 = whiskerRight θ.1 g.1
source
@[simp]
theorem CategoryTheory.Bicategory.prod_leftUnitor_hom_fst (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {a✝ b✝ : B × C} (f : a✝ ⟶ b✝) :
(leftUnitor f).hom.1 = (leftUnitor f.1).hom
source
@[simp]
theorem CategoryTheory.Bicategory.prod_rightUnitor_hom_fst (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {a✝ b✝ : B × C} (f : a✝ ⟶ b✝) :
(rightUnitor f).hom.1 = (rightUnitor f.1).hom
source
@[simp]
theorem CategoryTheory.Bicategory.prod_rightUnitor_hom_snd (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {a✝ b✝ : B × C} (f : a✝ ⟶ b✝) :
(rightUnitor f).hom.2 = (rightUnitor f.2).hom
source
@[simp]
theorem CategoryTheory.Bicategory.prod_rightUnitor_inv_snd (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {a✝ b✝ : B × C} (f : a✝ ⟶ b✝) :
(rightUnitor f).inv.2 = (rightUnitor f.2).inv
source
@[simp]
theorem CategoryTheory.Bicategory.prod_whiskerRight_snd (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {a✝ b✝ c✝ : B × C} {f✝ g✝ : a✝ ⟶ b✝} (θ : f✝ ⟶ g✝) (g : b✝ ⟶ c✝) :
(whiskerRight θ g).2 = whiskerRight θ.2 g.2
source
@[simp]
theorem CategoryTheory.Bicategory.prod_leftUnitor_inv_snd (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {a✝ b✝ : B × C} (f : a✝ ⟶ b✝) :
(leftUnitor f).inv.2 = (leftUnitor f.2).inv
source
@[simp]
theorem CategoryTheory.Bicategory.prod_associator_inv_snd (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {a✝ b✝ c✝ d✝ : B × C} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) (h : c✝ ⟶ d✝) :
(associator f g h).inv.2 = (associator f.2 g.2 h.2).inv
source
@[simp]
theorem CategoryTheory.Bicategory.prod_id_fst (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] (X : B × C) :
(CategoryStruct.id X).1 = CategoryStruct.id X.1
source
@[simp]
theorem CategoryTheory.Bicategory.prod_whiskerLeft_fst (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {a✝ b✝ c✝ : B × C} (f : a✝ ⟶ b✝) (g h : b✝ ⟶ c✝) (θ : g ⟶ h) :
(whiskerLeft f θ).1 = whiskerLeft f.1 θ.1
source
@[simp]
theorem CategoryTheory.Bicategory.prod_comp_snd (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {X✝ Y✝ Z✝ : B × C} (f : (X✝.1 ⟶ Y✝.1) × (X✝.2 ⟶ Y✝.2)) (g : (Y✝.1 ⟶ Z✝.1) × (Y✝.2 ⟶ Z✝.2)) :
(CategoryStruct.comp f g).2 = CategoryStruct.comp f.2 g.2
source
@[simp]
theorem CategoryTheory.Bicategory.prod_homCategory_comp_snd (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] (X Y : B × C) {X✝ Y✝ Z✝ : (X.1 ⟶ Y.1) × (X.2 ⟶ Y.2)} (f : (X✝.1 ⟶ Y✝.1) × (X✝.2 ⟶ Y✝.2)) (g : (Y✝.1 ⟶ Z✝.1) × (Y✝.2 ⟶ Z✝.2)) :
(CategoryStruct.comp f g).2 = CategoryStruct.comp f.2 g.2
source
@[simp]
theorem CategoryTheory.Bicategory.prod_leftUnitor_hom_snd (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {a✝ b✝ : B × C} (f : a✝ ⟶ b✝) :
(leftUnitor f).hom.2 = (leftUnitor f.2).hom
source
@[simp]
theorem CategoryTheory.Bicategory.prod_associator_inv_fst (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {a✝ b✝ c✝ d✝ : B × C} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) (h : c✝ ⟶ d✝) :
(associator f g h).inv.1 = (associator f.1 g.1 h.1).inv
source
@[simp]
theorem CategoryTheory.Bicategory.prod_Hom (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] (X Y : B × C) :
(X ⟶ Y) = ((X.1 ⟶ Y.1) × (X.2 ⟶ Y.2))
source
@[simp]
theorem CategoryTheory.Bicategory.prod_comp_fst (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {X✝ Y✝ Z✝ : B × C} (f : (X✝.1 ⟶ Y✝.1) × (X✝.2 ⟶ Y✝.2)) (g : (Y✝.1 ⟶ Z✝.1) × (Y✝.2 ⟶ Z✝.2)) :
(CategoryStruct.comp f g).1 = CategoryStruct.comp f.1 g.1
source
@[simp]
theorem CategoryTheory.Bicategory.prod_id_snd (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] (X : B × C) :
(CategoryStruct.id X).2 = CategoryStruct.id X.2
source
@[simp]
theorem CategoryTheory.Bicategory.prod_whiskerLeft_snd (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {a✝ b✝ c✝ : B × C} (f : a✝ ⟶ b✝) (g h : b✝ ⟶ c✝) (θ : g ⟶ h) :
(whiskerLeft f θ).2 = whiskerLeft f.2 θ.2
source
@[simp]
theorem CategoryTheory.Bicategory.prod_associator_hom_fst (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {a✝ b✝ c✝ d✝ : B × C} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) (h : c✝ ⟶ d✝) :
(associator f g h).hom.1 = (associator f.1 g.1 h.1).hom
source
@[simp]
theorem CategoryTheory.Bicategory.prod_rightUnitor_inv_fst (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {a✝ b✝ : B × C} (f : a✝ ⟶ b✝) :
(rightUnitor f).inv.1 = (rightUnitor f.1).inv
source
instance CategoryTheory.Bicategory.instStrictProd (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] [Strict B] [Strict C] :
Strict (B × C)

The cartesian product of two strict bicategories is strict.

source
def CategoryTheory.Bicategory.Prod.sectL (B : Type u₁) [Bicategory B] {C : Type u₂} [Bicategory C] (c : C) :
StrictlyUnitaryPseudofunctor B (B × C)

sectL B c is the strictly unitary pseudofunctor B ⥤ B × C given by X ↦ (X, c).

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CategoryTheory.Bicategory.Prod.sectL_mapId_hom (B : Type u₁) [Bicategory B] {C : Type u₂} [Bicategory C] (c : C) (x : B) :
    ((sectL B c).mapId x).hom = Prod.mkHom (CategoryStruct.id (CategoryStruct.id x)) (CategoryStruct.id (CategoryStruct.id c))
    source
    @[simp]
    theorem CategoryTheory.Bicategory.Prod.sectL_mapComp_hom (B : Type u₁) [Bicategory B] {C : Type u₂} [Bicategory C] (c : C) {a✝ b✝ c✝ : B} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) :
    ((sectL B c).mapComp f g).hom = Prod.mkHom (CategoryStruct.id (CategoryStruct.comp f g)) (rightUnitor (CategoryStruct.id c)).inv
    source
    @[simp]
    theorem CategoryTheory.Bicategory.Prod.sectL_map₂ (B : Type u₁) [Bicategory B] {C : Type u₂} [Bicategory C] (c : C) {a✝ b✝ : B} {f✝ g✝ : a✝ ⟶ b✝} (a✝¹ : f✝ ⟶ g✝) :
    (sectL B c).map₂ a✝¹ = Prod.mkHom a✝¹ (CategoryStruct.id (CategoryStruct.id c))
    source
    @[simp]
    theorem CategoryTheory.Bicategory.Prod.sectL_mapId_inv (B : Type u₁) [Bicategory B] {C : Type u₂} [Bicategory C] (c : C) (x : B) :
    ((sectL B c).mapId x).inv = Prod.mkHom (CategoryStruct.id (CategoryStruct.id x)) (CategoryStruct.id (CategoryStruct.id c))
    source
    @[simp]
    theorem CategoryTheory.Bicategory.Prod.sectL_map (B : Type u₁) [Bicategory B] {C : Type u₂} [Bicategory C] (c : C) {X✝ Y✝ : B} (a✝ : X✝ ⟶ Y✝) :
    (sectL B c).map a✝ = Prod.mkHom a✝ (CategoryStruct.id c)
    source
    @[simp]
    theorem CategoryTheory.Bicategory.Prod.sectL_obj (B : Type u₁) [Bicategory B] {C : Type u₂} [Bicategory C] (c : C) (a✝ : B) :
    (sectL B c).obj a✝ = (a✝, c)
    source
    @[simp]
    theorem CategoryTheory.Bicategory.Prod.sectL_mapComp_inv (B : Type u₁) [Bicategory B] {C : Type u₂} [Bicategory C] (c : C) {a✝ b✝ c✝ : B} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) :
    ((sectL B c).mapComp f g).inv = Prod.mkHom (CategoryStruct.id (CategoryStruct.comp f g)) (rightUnitor (CategoryStruct.id c)).hom
    source
    def CategoryTheory.Bicategory.Prod.sectR {B : Type u₁} [Bicategory B] (b : B) (C : Type u₂) [Bicategory C] :
    StrictlyUnitaryPseudofunctor C (B × C)

    sectR b C is the strictly unitary pseudofunctor C ⥤ B × C given by Y ↦ (b, Y).

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem CategoryTheory.Bicategory.Prod.sectR_obj {B : Type u₁} [Bicategory B] (b : B) (C : Type u₂) [Bicategory C] (a✝ : C) :
      (sectR b C).obj a✝ = (b, a✝)
      source
      @[simp]
      theorem CategoryTheory.Bicategory.Prod.sectR_mapId_inv {B : Type u₁} [Bicategory B] (b : B) (C : Type u₂) [Bicategory C] (x : C) :
      ((sectR b C).mapId x).inv = Prod.mkHom (CategoryStruct.id (CategoryStruct.id b)) (CategoryStruct.id (CategoryStruct.id x))
      source
      @[simp]
      theorem CategoryTheory.Bicategory.Prod.sectR_map₂ {B : Type u₁} [Bicategory B] (b : B) (C : Type u₂) [Bicategory C] {a✝ b✝ : C} {f✝ g✝ : a✝ ⟶ b✝} (a✝¹ : f✝ ⟶ g✝) :
      (sectR b C).map₂ a✝¹ = Prod.mkHom (CategoryStruct.id (CategoryStruct.id b)) a✝¹
      source
      @[simp]
      theorem CategoryTheory.Bicategory.Prod.sectR_map {B : Type u₁} [Bicategory B] (b : B) (C : Type u₂) [Bicategory C] {X✝ Y✝ : C} (a✝ : X✝ ⟶ Y✝) :
      (sectR b C).map a✝ = Prod.mkHom (CategoryStruct.id b) a✝
      source
      @[simp]
      theorem CategoryTheory.Bicategory.Prod.sectR_mapId_hom {B : Type u₁} [Bicategory B] (b : B) (C : Type u₂) [Bicategory C] (x : C) :
      ((sectR b C).mapId x).hom = Prod.mkHom (CategoryStruct.id (CategoryStruct.id b)) (CategoryStruct.id (CategoryStruct.id x))
      source
      @[simp]
      theorem CategoryTheory.Bicategory.Prod.sectR_mapComp_inv {B : Type u₁} [Bicategory B] (b : B) (C : Type u₂) [Bicategory C] {a✝ b✝ c✝ : C} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) :
      ((sectR b C).mapComp f g).inv = Prod.mkHom (rightUnitor (CategoryStruct.id b)).hom (CategoryStruct.id (CategoryStruct.comp f g))
      source
      @[simp]
      theorem CategoryTheory.Bicategory.Prod.sectR_mapComp_hom {B : Type u₁} [Bicategory B] (b : B) (C : Type u₂) [Bicategory C] {a✝ b✝ c✝ : C} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) :
      ((sectR b C).mapComp f g).hom = Prod.mkHom (rightUnitor (CategoryStruct.id b)).inv (CategoryStruct.id (CategoryStruct.comp f g))
      source
      def CategoryTheory.Bicategory.Prod.fst (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] :
      StrictPseudofunctor (B × C) B

      fst is the strict pseudofunctor given by projection to the first factor.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem CategoryTheory.Bicategory.Prod.fst_mapId_hom (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] (x : B × C) :
        ((fst B C).mapId x).hom = CategoryStruct.id (CategoryStruct.id x.1)
        source
        @[simp]
        theorem CategoryTheory.Bicategory.Prod.fst_map (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {X✝ Y✝ : B × C} (a✝ : X✝ ⟶ Y✝) :
        (fst B C).map a✝ = a✝.1
        source
        @[simp]
        theorem CategoryTheory.Bicategory.Prod.fst_mapComp_hom (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {a✝ b✝ c✝ : B × C} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) :
        ((fst B C).mapComp f g).hom = CategoryStruct.id (CategoryStruct.comp f.1 g.1)
        source
        @[simp]
        theorem CategoryTheory.Bicategory.Prod.fst_map₂ (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {a✝ b✝ : B × C} {f✝ g✝ : a✝ ⟶ b✝} (a✝¹ : f✝ ⟶ g✝) :
        (fst B C).map₂ a✝¹ = a✝¹.1
        source
        @[simp]
        theorem CategoryTheory.Bicategory.Prod.fst_obj (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] (a✝ : B × C) :
        (fst B C).obj a✝ = a✝.1
        source
        @[simp]
        theorem CategoryTheory.Bicategory.Prod.fst_mapComp_inv (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {a✝ b✝ c✝ : B × C} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) :
        ((fst B C).mapComp f g).inv = CategoryStruct.id (CategoryStruct.comp f.1 g.1)
        source
        @[simp]
        theorem CategoryTheory.Bicategory.Prod.fst_mapId_inv (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] (x : B × C) :
        ((fst B C).mapId x).inv = CategoryStruct.id (CategoryStruct.id x.1)
        source
        def CategoryTheory.Bicategory.Prod.snd (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] :
        StrictPseudofunctor (B × C) C

        snd is the strict pseudofunctor given by projection to the second factor.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem CategoryTheory.Bicategory.Prod.snd_mapId_inv (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] (x : B × C) :
          ((snd B C).mapId x).inv = CategoryStruct.id (CategoryStruct.id x.2)
          source
          @[simp]
          theorem CategoryTheory.Bicategory.Prod.snd_mapId_hom (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] (x : B × C) :
          ((snd B C).mapId x).hom = CategoryStruct.id (CategoryStruct.id x.2)
          source
          @[simp]
          theorem CategoryTheory.Bicategory.Prod.snd_mapComp_hom (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {a✝ b✝ c✝ : B × C} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) :
          ((snd B C).mapComp f g).hom = CategoryStruct.id (CategoryStruct.comp f.2 g.2)
          source
          @[simp]
          theorem CategoryTheory.Bicategory.Prod.snd_obj (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] (a✝ : B × C) :
          (snd B C).obj a✝ = a✝.2
          source
          @[simp]
          theorem CategoryTheory.Bicategory.Prod.snd_mapComp_inv (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {a✝ b✝ c✝ : B × C} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) :
          ((snd B C).mapComp f g).inv = CategoryStruct.id (CategoryStruct.comp f.2 g.2)
          source
          @[simp]
          theorem CategoryTheory.Bicategory.Prod.snd_map (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {X✝ Y✝ : B × C} (a✝ : X✝ ⟶ Y✝) :
          (snd B C).map a✝ = a✝.2
          source
          @[simp]
          theorem CategoryTheory.Bicategory.Prod.snd_map₂ (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {a✝ b✝ : B × C} {f✝ g✝ : a✝ ⟶ b✝} (a✝¹ : f✝ ⟶ g✝) :
          (snd B C).map₂ a✝¹ = a✝¹.2
          source
          def CategoryTheory.Bicategory.Prod.swap (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] :
          StrictPseudofunctor (B × C) (C × B)

          The pseudofunctor swapping the factors of a cartesian product of bicategories, B × C ⥤ C × B.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem CategoryTheory.Bicategory.Prod.swap_obj (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] (a✝ : B × C) :
            (swap B C).obj a✝ = (a✝.2, a✝.1)
            source
            @[simp]
            theorem CategoryTheory.Bicategory.Prod.swap_mapId_inv (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] (x : B × C) :
            ((swap B C).mapId x).inv = Prod.mkHom (CategoryStruct.id (CategoryStruct.id x.2)) (CategoryStruct.id (CategoryStruct.id x.1))
            source
            @[simp]
            theorem CategoryTheory.Bicategory.Prod.swap_mapComp_hom (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {a✝ b✝ c✝ : B × C} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) :
            ((swap B C).mapComp f g).hom = Prod.mkHom (CategoryStruct.id (CategoryStruct.comp f.2 g.2)) (CategoryStruct.id (CategoryStruct.comp f.1 g.1))
            source
            @[simp]
            theorem CategoryTheory.Bicategory.Prod.swap_map₂ (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {a✝ b✝ : B × C} {f✝ g✝ : a✝ ⟶ b✝} (a✝¹ : f✝ ⟶ g✝) :
            (swap B C).map₂ a✝¹ = Prod.mkHom a✝¹.2 a✝¹.1
            source
            @[simp]
            theorem CategoryTheory.Bicategory.Prod.swap_map (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {X✝ Y✝ : B × C} (a✝ : X✝ ⟶ Y✝) :
            (swap B C).map a✝ = Prod.mkHom a✝.2 a✝.1
            source
            @[simp]
            theorem CategoryTheory.Bicategory.Prod.swap_mapComp_inv (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] {a✝ b✝ c✝ : B × C} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) :
            ((swap B C).mapComp f g).inv = Prod.mkHom (CategoryStruct.id (CategoryStruct.comp f.2 g.2)) (CategoryStruct.id (CategoryStruct.comp f.1 g.1))
            source
            @[simp]
            theorem CategoryTheory.Bicategory.Prod.swap_mapId_hom (B : Type u₁) [Bicategory B] (C : Type u₂) [Bicategory C] (x : B × C) :
            ((swap B C).mapId x).hom = Prod.mkHom (CategoryStruct.id (CategoryStruct.id x.2)) (CategoryStruct.id (CategoryStruct.id x.1))
            source
            @[instance_reducible]
            instance CategoryTheory.Bicategory.uniformProd (B : Type u₁) [Bicategory B] (C : Type u₁) [Bicategory C] :
            Bicategory (B × C)

            Bicategory.uniformProd B C is an additional instance specialised so both factors have the same universe levels. This helps typeclass resolution.

            Equations