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} [Bicategory B] {a b : B} (f 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.

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

Notation for identities up to unitors and associators.

@[reducible, inline]

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

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

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

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

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

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

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

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

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

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

@[simp]

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