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.

• hom : f ⟶ g

  The chosen structural isomorphism between to 1-morphisms.

• isIso : CategoryTheory.IsIso CategoryTheory.BicategoricalCoherence.hom

theorem CategoryTheory.BicategoricalCoherence.isIso {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {f : a ⟶ b} {g : a ⟶ b} [self : CategoryTheory.BicategoricalCoherence f g] : CategoryTheory.IsIso CategoryTheory.BicategoricalCoherence.hom

def CategoryTheory.Bicategory.«term⊗𝟙» : Lean.ParserDescr

Notation for identities up to unitors and associators.

Equations

• CategoryTheory.Bicategory.«term⊗𝟙» = Lean.ParserDescr.node `CategoryTheory.Bicategory.term⊗𝟙 1024 (Lean.ParserDescr.symbol " ⊗𝟙 ")

def 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.asIso CategoryTheory.BicategoricalCoherence.hom

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.hom θ)

def CategoryTheory.Bicategory.«term_⊗≫_» : Lean.TrailingParserDescr

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

Equations

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

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.asIso CategoryTheory.BicategoricalCoherence.hom ≪≫ θ

def CategoryTheory.Bicategory.«term_≪⊗≫_» : Lean.TrailingParserDescr

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

Equations

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

@[simp]

theorem CategoryTheory.BicategoricalCoherence.refl_hom {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} (f : a ⟶ b) : CategoryTheory.BicategoricalCoherence.hom = CategoryTheory.CategoryStruct.id f

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 = CategoryTheory.BicategoricalCoherence.mk (CategoryTheory.CategoryStruct.id f)

@[simp]

theorem CategoryTheory.BicategoricalCoherence.whiskerLeft_hom {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.hom = CategoryTheory.Bicategory.whiskerLeft f CategoryTheory.BicategoricalCoherence.hom

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 = CategoryTheory.BicategoricalCoherence.mk (CategoryTheory.Bicategory.whiskerLeft f CategoryTheory.BicategoricalCoherence.hom)

@[simp]

theorem CategoryTheory.BicategoricalCoherence.whiskerRight_hom {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.hom = CategoryTheory.Bicategory.whiskerRight CategoryTheory.BicategoricalCoherence.hom h

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 = CategoryTheory.BicategoricalCoherence.mk (CategoryTheory.Bicategory.whiskerRight CategoryTheory.BicategoricalCoherence.hom h)

@[simp]

theorem CategoryTheory.BicategoricalCoherence.tensorRight_hom {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.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor f).inv (CategoryTheory.Bicategory.whiskerLeft f CategoryTheory.BicategoricalCoherence.hom)

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'_hom {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.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f CategoryTheory.BicategoricalCoherence.hom) (CategoryTheory.Bicategory.rightUnitor f).hom

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.left_hom {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} (f : a ⟶ b) (g : a ⟶ b) [CategoryTheory.BicategoricalCoherence f g] : CategoryTheory.BicategoricalCoherence.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor f).hom CategoryTheory.BicategoricalCoherence.hom

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

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

@[simp]

theorem CategoryTheory.BicategoricalCoherence.left'_hom {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} (f : a ⟶ b) (g : a ⟶ b) [CategoryTheory.BicategoricalCoherence f g] : CategoryTheory.BicategoricalCoherence.hom = CategoryTheory.CategoryStruct.comp CategoryTheory.BicategoricalCoherence.hom (CategoryTheory.Bicategory.leftUnitor g).inv

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

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

@[simp]

theorem CategoryTheory.BicategoricalCoherence.right_hom {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} (f : a ⟶ b) (g : a ⟶ b) [CategoryTheory.BicategoricalCoherence f g] : CategoryTheory.BicategoricalCoherence.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor f).hom CategoryTheory.BicategoricalCoherence.hom

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

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

@[simp]

theorem CategoryTheory.BicategoricalCoherence.right'_hom {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} (f : a ⟶ b) (g : a ⟶ b) [CategoryTheory.BicategoricalCoherence f g] : CategoryTheory.BicategoricalCoherence.hom = CategoryTheory.CategoryStruct.comp CategoryTheory.BicategoricalCoherence.hom (CategoryTheory.Bicategory.rightUnitor g).inv

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

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

@[simp]

theorem CategoryTheory.BicategoricalCoherence.assoc_hom {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.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h).hom CategoryTheory.BicategoricalCoherence.hom

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

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

@[simp]

theorem CategoryTheory.BicategoricalCoherence.assoc'_hom {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.hom = CategoryTheory.CategoryStruct.comp CategoryTheory.BicategoricalCoherence.hom (CategoryTheory.Bicategory.associator f g h).inv

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

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

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