Bicategorical composition ⊗≫ (composition up to associators)

We provide f ⊗≫ g, the bicategoricalComp operation, which automatically inserts associators and unitors as needed to make the target of f match the source of g.

class CategoryTheory.BicategoricalCoherence {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} (f : a ⟶ b) (g : a ⟶ b) : Type w

A typeclass carrying a choice of bicategorical structural isomorphism between two objects. Used by the ⊗≫ bicategorical composition operator, and the coherence tactic.

• iso : f ≅ g

  The chosen structural isomorphism between to 1-morphisms.

@[reducible, inline]

abbrev CategoryTheory.bicategoricalIso {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} (f : a ⟶ b) (g : a ⟶ b) [CategoryTheory.BicategoricalCoherence f g] : f ≅ g

Construct an isomorphism between two objects in a bicategorical category out of unitors and associators.

Equations

• CategoryTheory.bicategoricalIso f g = CategoryTheory.BicategoricalCoherence.iso

def CategoryTheory.bicategoricalComp {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {f : a ⟶ b} {g : a ⟶ b} {h : a ⟶ b} {i : a ⟶ b} [CategoryTheory.BicategoricalCoherence g h] (η : f ⟶ g) (θ : h ⟶ i) : f ⟶ i

Compose two morphisms in a bicategorical category, inserting unitors and associators between as necessary.

Equations

• CategoryTheory.bicategoricalComp η θ = CategoryTheory.CategoryStruct.comp η (CategoryTheory.CategoryStruct.comp CategoryTheory.BicategoricalCoherence.iso.hom θ)

def CategoryTheory.bicategoricalIsoComp {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {f : a ⟶ b} {g : a ⟶ b} {h : a ⟶ b} {i : a ⟶ b} [CategoryTheory.BicategoricalCoherence g h] (η : f ≅ g) (θ : h ≅ i) : f ≅ i

Compose two isomorphisms in a bicategorical category, inserting unitors and associators between as necessary.

Equations

• CategoryTheory.bicategoricalIsoComp η θ = η ≪≫ CategoryTheory.BicategoricalCoherence.iso ≪≫ θ

instance CategoryTheory.BicategoricalCoherence.refl {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} (f : a ⟶ b) : CategoryTheory.BicategoricalCoherence f f

Equations

• CategoryTheory.BicategoricalCoherence.refl f = { iso := CategoryTheory.Iso.refl f }

@[simp]

theorem CategoryTheory.BicategoricalCoherence.refl_iso {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} (f : a ⟶ b) : CategoryTheory.BicategoricalCoherence.iso = CategoryTheory.Iso.refl f

instance CategoryTheory.BicategoricalCoherence.whiskerLeft {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} (f : a ⟶ b) (g : b ⟶ c) (h : b ⟶ c) [CategoryTheory.BicategoricalCoherence g h] : CategoryTheory.BicategoricalCoherence (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.comp f h)

Equations

• CategoryTheory.BicategoricalCoherence.whiskerLeft f g h = { iso := CategoryTheory.Bicategory.whiskerLeftIso f CategoryTheory.BicategoricalCoherence.iso }

@[simp]

theorem CategoryTheory.BicategoricalCoherence.whiskerLeft_iso {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} (f : a ⟶ b) (g : b ⟶ c) (h : b ⟶ c) [CategoryTheory.BicategoricalCoherence g h] : CategoryTheory.BicategoricalCoherence.iso = CategoryTheory.Bicategory.whiskerLeftIso f CategoryTheory.BicategoricalCoherence.iso

instance CategoryTheory.BicategoricalCoherence.whiskerRight {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} (f : a ⟶ b) (g : a ⟶ b) (h : b ⟶ c) [CategoryTheory.BicategoricalCoherence f g] : CategoryTheory.BicategoricalCoherence (CategoryTheory.CategoryStruct.comp f h) (CategoryTheory.CategoryStruct.comp g h)

Equations

• CategoryTheory.BicategoricalCoherence.whiskerRight f g h = { iso := CategoryTheory.Bicategory.whiskerRightIso CategoryTheory.BicategoricalCoherence.iso h }

@[simp]

theorem CategoryTheory.BicategoricalCoherence.whiskerRight_iso {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} (f : a ⟶ b) (g : a ⟶ b) (h : b ⟶ c) [CategoryTheory.BicategoricalCoherence f g] : CategoryTheory.BicategoricalCoherence.iso = CategoryTheory.Bicategory.whiskerRightIso CategoryTheory.BicategoricalCoherence.iso h

instance CategoryTheory.BicategoricalCoherence.tensorRight {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} (f : a ⟶ b) (g : b ⟶ b) [CategoryTheory.BicategoricalCoherence (CategoryTheory.CategoryStruct.id b) g] : CategoryTheory.BicategoricalCoherence f (CategoryTheory.CategoryStruct.comp f g)

Equations

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

@[simp]

theorem CategoryTheory.BicategoricalCoherence.tensorRight_iso {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} (f : a ⟶ b) (g : b ⟶ b) [CategoryTheory.BicategoricalCoherence (CategoryTheory.CategoryStruct.id b) g] : CategoryTheory.BicategoricalCoherence.iso = (CategoryTheory.Bicategory.rightUnitor f).symm ≪≫ CategoryTheory.Bicategory.whiskerLeftIso f CategoryTheory.BicategoricalCoherence.iso

instance CategoryTheory.BicategoricalCoherence.tensorRight' {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} (f : a ⟶ b) (g : b ⟶ b) [CategoryTheory.BicategoricalCoherence g (CategoryTheory.CategoryStruct.id b)] : CategoryTheory.BicategoricalCoherence (CategoryTheory.CategoryStruct.comp f g) f

Equations

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

@[simp]

theorem CategoryTheory.BicategoricalCoherence.tensorRight'_iso {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} (f : a ⟶ b) (g : b ⟶ b) [CategoryTheory.BicategoricalCoherence g (CategoryTheory.CategoryStruct.id b)] : CategoryTheory.BicategoricalCoherence.iso = CategoryTheory.Bicategory.whiskerLeftIso f CategoryTheory.BicategoricalCoherence.iso ≪≫ CategoryTheory.Bicategory.rightUnitor f

instance CategoryTheory.BicategoricalCoherence.left {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} (f : a ⟶ b) (g : a ⟶ b) [CategoryTheory.BicategoricalCoherence f g] : CategoryTheory.BicategoricalCoherence (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id a) f) g

Equations

• CategoryTheory.BicategoricalCoherence.left f g = { iso := CategoryTheory.Bicategory.leftUnitor f ≪≫ CategoryTheory.BicategoricalCoherence.iso }

@[simp]

theorem CategoryTheory.BicategoricalCoherence.left_iso {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} (f : a ⟶ b) (g : a ⟶ b) [CategoryTheory.BicategoricalCoherence f g] : CategoryTheory.BicategoricalCoherence.iso = CategoryTheory.Bicategory.leftUnitor f ≪≫ CategoryTheory.BicategoricalCoherence.iso

instance CategoryTheory.BicategoricalCoherence.left' {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} (f : a ⟶ b) (g : a ⟶ b) [CategoryTheory.BicategoricalCoherence f g] : CategoryTheory.BicategoricalCoherence f (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id a) g)

Equations

• CategoryTheory.BicategoricalCoherence.left' f g = { iso := CategoryTheory.BicategoricalCoherence.iso ≪≫ (CategoryTheory.Bicategory.leftUnitor g).symm }

@[simp]

theorem CategoryTheory.BicategoricalCoherence.left'_iso {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} (f : a ⟶ b) (g : a ⟶ b) [CategoryTheory.BicategoricalCoherence f g] : CategoryTheory.BicategoricalCoherence.iso = CategoryTheory.BicategoricalCoherence.iso ≪≫ (CategoryTheory.Bicategory.leftUnitor g).symm

instance CategoryTheory.BicategoricalCoherence.right {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} (f : a ⟶ b) (g : a ⟶ b) [CategoryTheory.BicategoricalCoherence f g] : CategoryTheory.BicategoricalCoherence (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id b)) g

Equations

• CategoryTheory.BicategoricalCoherence.right f g = { iso := CategoryTheory.Bicategory.rightUnitor f ≪≫ CategoryTheory.BicategoricalCoherence.iso }

@[simp]

theorem CategoryTheory.BicategoricalCoherence.right_iso {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} (f : a ⟶ b) (g : a ⟶ b) [CategoryTheory.BicategoricalCoherence f g] : CategoryTheory.BicategoricalCoherence.iso = CategoryTheory.Bicategory.rightUnitor f ≪≫ CategoryTheory.BicategoricalCoherence.iso

instance CategoryTheory.BicategoricalCoherence.right' {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} (f : a ⟶ b) (g : a ⟶ b) [CategoryTheory.BicategoricalCoherence f g] : CategoryTheory.BicategoricalCoherence f (CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.id b))

Equations

• CategoryTheory.BicategoricalCoherence.right' f g = { iso := CategoryTheory.BicategoricalCoherence.iso ≪≫ (CategoryTheory.Bicategory.rightUnitor g).symm }

@[simp]

theorem CategoryTheory.BicategoricalCoherence.right'_iso {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} (f : a ⟶ b) (g : a ⟶ b) [CategoryTheory.BicategoricalCoherence f g] : CategoryTheory.BicategoricalCoherence.iso = CategoryTheory.BicategoricalCoherence.iso ≪≫ (CategoryTheory.Bicategory.rightUnitor g).symm

instance CategoryTheory.BicategoricalCoherence.assoc {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : a ⟶ d) [CategoryTheory.BicategoricalCoherence (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h)) i] : CategoryTheory.BicategoricalCoherence (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h) i

Equations

• CategoryTheory.BicategoricalCoherence.assoc f g h i = { iso := CategoryTheory.Bicategory.associator f g h ≪≫ CategoryTheory.BicategoricalCoherence.iso }

@[simp]

theorem CategoryTheory.BicategoricalCoherence.assoc_iso {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : a ⟶ d) [CategoryTheory.BicategoricalCoherence (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h)) i] : CategoryTheory.BicategoricalCoherence.iso = CategoryTheory.Bicategory.associator f g h ≪≫ CategoryTheory.BicategoricalCoherence.iso

instance CategoryTheory.BicategoricalCoherence.assoc' {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : a ⟶ d) [CategoryTheory.BicategoricalCoherence i (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h))] : CategoryTheory.BicategoricalCoherence i (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h)

Equations

• CategoryTheory.BicategoricalCoherence.assoc' f g h i = { iso := CategoryTheory.BicategoricalCoherence.iso ≪≫ (CategoryTheory.Bicategory.associator f g h).symm }

@[simp]

theorem CategoryTheory.BicategoricalCoherence.assoc'_iso {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : a ⟶ d) [CategoryTheory.BicategoricalCoherence i (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h))] : CategoryTheory.BicategoricalCoherence.iso = CategoryTheory.BicategoricalCoherence.iso ≪≫ (CategoryTheory.Bicategory.associator f g h).symm

@[simp]

theorem CategoryTheory.bicategoricalComp_refl {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {f : a ⟶ b} {g : a ⟶ b} {h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h) : CategoryTheory.bicategoricalComp η θ = CategoryTheory.CategoryStruct.comp η θ