Cartesian products of bicategories #

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

We define:

sectL B c : the strictly unitary pseudofunctor B ⥤ B × C given by X ↦ ⟨X, c⟩
sectR b C : the strictly unitary pseudofunctor C ⥤ B × C given by Y ↦ ⟨b, Y⟩
fst : the strict pseudofunctor ⟨X, Y⟩ ↦ X
snd : the strict pseudofunctor ⟨X, Y⟩ ↦ Y
swap : the strict pseudofunctor B × C ⥤ C × B given by ⟨X, Y⟩ ↦ ⟨Y, X⟩

source

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

Bicategory (B × C)

The cartesian product of two bicategories.

Equations

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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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_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

@[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

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

Instances For

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

@[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_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_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_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

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

Instances For

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_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_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

@[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_obj {B : Type u₁} [Bicategory B] (b : B) (C : Type u₂) [Bicategory C] (a✝ : C) :

(sectR b C).obj a✝ = (b, a✝)

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

Instances For

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_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_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_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_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

@[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

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

Instances For

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_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_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_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_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_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] {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

Instances For

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

@[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_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_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_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_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_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

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

Documentation

Mathlib.CategoryTheory.Bicategory.Product

Cartesian products of bicategories #