A coherence tactic for bicategories, and ⊗≫ (composition up to associators)

We provide a bicategory_coherence tactic, which proves that any two 2-morphisms (with the same source and target) in a bicategory which are built out of associators and unitors are equal.

We also 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.

This file mainly deals with the type class setup for the coherence tactic. The actual front end tactic is given in Mathlib.Tactic.CategoryTheory.Coherence at the same time as the coherence tactic for monoidal categories.

class Mathlib.Tactic.BicategoryCoherence.LiftHom {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} (f : a ⟶ b) : Type (max u v)

• lift : CategoryTheory.FreeBicategory.of.obj a ⟶ CategoryTheory.FreeBicategory.of.obj b

  A lift of a morphism to the free bicategory. This should only exist for "structural" morphisms.

A typeclass carrying a choice of lift of a 1-morphism from B to FreeBicategory B.

instance Mathlib.Tactic.BicategoryCoherence.liftHomId {B : Type u} [CategoryTheory.Bicategory B] {a : B} : Mathlib.Tactic.BicategoryCoherence.LiftHom (CategoryTheory.CategoryStruct.id a)

instance Mathlib.Tactic.BicategoryCoherence.liftHomComp {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} (f : a ⟶ b) (g : b ⟶ c) [Mathlib.Tactic.BicategoryCoherence.LiftHom f] [Mathlib.Tactic.BicategoryCoherence.LiftHom g] : Mathlib.Tactic.BicategoryCoherence.LiftHom (CategoryTheory.CategoryStruct.comp f g)

instance Mathlib.Tactic.BicategoryCoherence.liftHomOf {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} (f : a ⟶ b) : Mathlib.Tactic.BicategoryCoherence.LiftHom f

class Mathlib.Tactic.BicategoryCoherence.LiftHom₂ {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {f : a ⟶ b} {g : a ⟶ b} [Mathlib.Tactic.BicategoryCoherence.LiftHom f] [Mathlib.Tactic.BicategoryCoherence.LiftHom g] (η : f ⟶ g) : Type (max u v)

• lift : Mathlib.Tactic.BicategoryCoherence.LiftHom.lift f ⟶ Mathlib.Tactic.BicategoryCoherence.LiftHom.lift g

  A lift of a 2-morphism to the free bicategory. This should only exist for "structural" 2-morphisms.

A typeclass carrying a choice of lift of a 2-morphism from B to FreeBicategory B.

instance Mathlib.Tactic.BicategoryCoherence.liftHom₂Id {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} (f : a ⟶ b) [Mathlib.Tactic.BicategoryCoherence.LiftHom f] : Mathlib.Tactic.BicategoryCoherence.LiftHom₂ (CategoryTheory.CategoryStruct.id f)

instance Mathlib.Tactic.BicategoryCoherence.liftHom₂LeftUnitorHom {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} (f : a ⟶ b) [Mathlib.Tactic.BicategoryCoherence.LiftHom f] : Mathlib.Tactic.BicategoryCoherence.LiftHom₂ (CategoryTheory.Bicategory.leftUnitor f).hom

instance Mathlib.Tactic.BicategoryCoherence.liftHom₂LeftUnitorInv {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} (f : a ⟶ b) [Mathlib.Tactic.BicategoryCoherence.LiftHom f] : Mathlib.Tactic.BicategoryCoherence.LiftHom₂ (CategoryTheory.Bicategory.leftUnitor f).inv

instance Mathlib.Tactic.BicategoryCoherence.liftHom₂RightUnitorHom {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} (f : a ⟶ b) [Mathlib.Tactic.BicategoryCoherence.LiftHom f] : Mathlib.Tactic.BicategoryCoherence.LiftHom₂ (CategoryTheory.Bicategory.rightUnitor f).hom

instance Mathlib.Tactic.BicategoryCoherence.liftHom₂RightUnitorInv {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} (f : a ⟶ b) [Mathlib.Tactic.BicategoryCoherence.LiftHom f] : Mathlib.Tactic.BicategoryCoherence.LiftHom₂ (CategoryTheory.Bicategory.rightUnitor f).inv

instance Mathlib.Tactic.BicategoryCoherence.liftHom₂AssociatorHom {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) [Mathlib.Tactic.BicategoryCoherence.LiftHom f] [Mathlib.Tactic.BicategoryCoherence.LiftHom g] [Mathlib.Tactic.BicategoryCoherence.LiftHom h] : Mathlib.Tactic.BicategoryCoherence.LiftHom₂ (CategoryTheory.Bicategory.associator f g h).hom

instance Mathlib.Tactic.BicategoryCoherence.liftHom₂AssociatorInv {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) [Mathlib.Tactic.BicategoryCoherence.LiftHom f] [Mathlib.Tactic.BicategoryCoherence.LiftHom g] [Mathlib.Tactic.BicategoryCoherence.LiftHom h] : Mathlib.Tactic.BicategoryCoherence.LiftHom₂ (CategoryTheory.Bicategory.associator f g h).inv

instance Mathlib.Tactic.BicategoryCoherence.liftHom₂Comp {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {f : a ⟶ b} {g : a ⟶ b} {h : a ⟶ b} [Mathlib.Tactic.BicategoryCoherence.LiftHom f] [Mathlib.Tactic.BicategoryCoherence.LiftHom g] [Mathlib.Tactic.BicategoryCoherence.LiftHom h] (η : f ⟶ g) (θ : g ⟶ h) [Mathlib.Tactic.BicategoryCoherence.LiftHom₂ η] [Mathlib.Tactic.BicategoryCoherence.LiftHom₂ θ] : Mathlib.Tactic.BicategoryCoherence.LiftHom₂ (CategoryTheory.CategoryStruct.comp η θ)

instance Mathlib.Tactic.BicategoryCoherence.liftHom₂WhiskerLeft {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} (f : a ⟶ b) [Mathlib.Tactic.BicategoryCoherence.LiftHom f] {g : b ⟶ c} {h : b ⟶ c} (η : g ⟶ h) [Mathlib.Tactic.BicategoryCoherence.LiftHom g] [Mathlib.Tactic.BicategoryCoherence.LiftHom h] [Mathlib.Tactic.BicategoryCoherence.LiftHom₂ η] : Mathlib.Tactic.BicategoryCoherence.LiftHom₂ (CategoryTheory.Bicategory.whiskerLeft f η)

instance Mathlib.Tactic.BicategoryCoherence.liftHom₂WhiskerRight {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {f : a ⟶ b} {g : a ⟶ b} (η : f ⟶ g) [Mathlib.Tactic.BicategoryCoherence.LiftHom f] [Mathlib.Tactic.BicategoryCoherence.LiftHom g] [Mathlib.Tactic.BicategoryCoherence.LiftHom₂ η] {h : b ⟶ c} [Mathlib.Tactic.BicategoryCoherence.LiftHom h] : Mathlib.Tactic.BicategoryCoherence.LiftHom₂ (CategoryTheory.Bicategory.whiskerRight η h)

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

• hom' : f ⟶ g

  The chosen structural isomorphism between to 1-morphisms.

• isIso : CategoryTheory.IsIso Mathlib.Tactic.BicategoryCoherence.BicategoricalCoherence.hom'

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

@[reducible]

def Mathlib.Tactic.BicategoryCoherence.BicategoricalCoherence.hom {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} (f : a ⟶ b) (g : a ⟶ b) [Mathlib.Tactic.BicategoryCoherence.LiftHom f] [Mathlib.Tactic.BicategoryCoherence.LiftHom g] [Mathlib.Tactic.BicategoryCoherence.BicategoricalCoherence f g] : f ⟶ g

The chosen structural isomorphism between to 1-morphisms.

@[simp]

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

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

@[simp]

theorem Mathlib.Tactic.BicategoryCoherence.BicategoricalCoherence.whiskerLeft_hom' {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} (f : a ⟶ b) (g : b ⟶ c) (h : b ⟶ c) [Mathlib.Tactic.BicategoryCoherence.LiftHom f] [Mathlib.Tactic.BicategoryCoherence.LiftHom g] [Mathlib.Tactic.BicategoryCoherence.LiftHom h] [Mathlib.Tactic.BicategoryCoherence.BicategoricalCoherence g h] : Mathlib.Tactic.BicategoryCoherence.BicategoricalCoherence.hom' = CategoryTheory.Bicategory.whiskerLeft f (Mathlib.Tactic.BicategoryCoherence.BicategoricalCoherence.hom g h)

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

@[simp]

theorem Mathlib.Tactic.BicategoryCoherence.BicategoricalCoherence.whiskerRight_hom' {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} (f : a ⟶ b) (g : a ⟶ b) (h : b ⟶ c) [Mathlib.Tactic.BicategoryCoherence.LiftHom f] [Mathlib.Tactic.BicategoryCoherence.LiftHom g] [Mathlib.Tactic.BicategoryCoherence.LiftHom h] [Mathlib.Tactic.BicategoryCoherence.BicategoricalCoherence f g] : Mathlib.Tactic.BicategoryCoherence.BicategoricalCoherence.hom' = CategoryTheory.Bicategory.whiskerRight (Mathlib.Tactic.BicategoryCoherence.BicategoricalCoherence.hom f g) h

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

@[simp]

theorem Mathlib.Tactic.BicategoryCoherence.BicategoricalCoherence.tensorRight_hom' {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} (f : a ⟶ b) (g : b ⟶ b) [Mathlib.Tactic.BicategoryCoherence.LiftHom f] [Mathlib.Tactic.BicategoryCoherence.LiftHom g] [Mathlib.Tactic.BicategoryCoherence.BicategoricalCoherence (CategoryTheory.CategoryStruct.id b) g] : Mathlib.Tactic.BicategoryCoherence.BicategoricalCoherence.hom' = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor f).inv (CategoryTheory.Bicategory.whiskerLeft f (Mathlib.Tactic.BicategoryCoherence.BicategoricalCoherence.hom (CategoryTheory.CategoryStruct.id b) g))

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

@[simp]

theorem Mathlib.Tactic.BicategoryCoherence.BicategoricalCoherence.tensorRight'_hom' {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} (f : a ⟶ b) (g : b ⟶ b) [Mathlib.Tactic.BicategoryCoherence.LiftHom f] [Mathlib.Tactic.BicategoryCoherence.LiftHom g] [Mathlib.Tactic.BicategoryCoherence.BicategoricalCoherence g (CategoryTheory.CategoryStruct.id b)] : Mathlib.Tactic.BicategoryCoherence.BicategoricalCoherence.hom' = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (Mathlib.Tactic.BicategoryCoherence.BicategoricalCoherence.hom g (CategoryTheory.CategoryStruct.id b))) (CategoryTheory.Bicategory.rightUnitor f).hom

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

@[simp]

theorem Mathlib.Tactic.BicategoryCoherence.BicategoricalCoherence.left_hom' {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} (f : a ⟶ b) (g : a ⟶ b) [Mathlib.Tactic.BicategoryCoherence.LiftHom f] [Mathlib.Tactic.BicategoryCoherence.LiftHom g] [Mathlib.Tactic.BicategoryCoherence.BicategoricalCoherence f g] : Mathlib.Tactic.BicategoryCoherence.BicategoricalCoherence.hom' = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor f).hom (Mathlib.Tactic.BicategoryCoherence.BicategoricalCoherence.hom f g)

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

theorem Mathlib.Tactic.BicategoryCoherence.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) [Mathlib.Tactic.BicategoryCoherence.LiftHom f] [Mathlib.Tactic.BicategoryCoherence.LiftHom g] [Mathlib.Tactic.BicategoryCoherence.LiftHom h] [Mathlib.Tactic.BicategoryCoherence.LiftHom i] [Mathlib.Tactic.BicategoryCoherence.BicategoricalCoherence (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h)) i] : Mathlib.Tactic.BicategoryCoherence.BicategoricalCoherence.hom' = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h).hom (Mathlib.Tactic.BicategoryCoherence.BicategoricalCoherence.hom (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h)) i)

instance Mathlib.Tactic.BicategoryCoherence.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) [Mathlib.Tactic.BicategoryCoherence.LiftHom f] [Mathlib.Tactic.BicategoryCoherence.LiftHom g] [Mathlib.Tactic.BicategoryCoherence.LiftHom h] [Mathlib.Tactic.BicategoryCoherence.LiftHom i] [Mathlib.Tactic.BicategoryCoherence.BicategoricalCoherence (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h)) i] : Mathlib.Tactic.BicategoryCoherence.BicategoricalCoherence (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h) i

@[simp]

theorem Mathlib.Tactic.BicategoryCoherence.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) [Mathlib.Tactic.BicategoryCoherence.LiftHom f] [Mathlib.Tactic.BicategoryCoherence.LiftHom g] [Mathlib.Tactic.BicategoryCoherence.LiftHom h] [Mathlib.Tactic.BicategoryCoherence.LiftHom i] [Mathlib.Tactic.BicategoryCoherence.BicategoricalCoherence i (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h))] : Mathlib.Tactic.BicategoryCoherence.BicategoricalCoherence.hom' = CategoryTheory.CategoryStruct.comp (Mathlib.Tactic.BicategoryCoherence.BicategoricalCoherence.hom i (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h))) (CategoryTheory.Bicategory.associator f g h).inv

instance Mathlib.Tactic.BicategoryCoherence.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) [Mathlib.Tactic.BicategoryCoherence.LiftHom f] [Mathlib.Tactic.BicategoryCoherence.LiftHom g] [Mathlib.Tactic.BicategoryCoherence.LiftHom h] [Mathlib.Tactic.BicategoryCoherence.LiftHom i] [Mathlib.Tactic.BicategoryCoherence.BicategoricalCoherence i (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h))] : Mathlib.Tactic.BicategoryCoherence.BicategoricalCoherence i (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h)

def Mathlib.Tactic.BicategoryCoherence.bicategoricalIso {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} (f : a ⟶ b) (g : a ⟶ b) [Mathlib.Tactic.BicategoryCoherence.LiftHom f] [Mathlib.Tactic.BicategoryCoherence.LiftHom g] [Mathlib.Tactic.BicategoryCoherence.BicategoricalCoherence f g] : f ≅ g

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

def Mathlib.Tactic.BicategoryCoherence.bicategoricalComp {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {f : a ⟶ b} {g : a ⟶ b} {h : a ⟶ b} {i : a ⟶ b} [Mathlib.Tactic.BicategoryCoherence.LiftHom g] [Mathlib.Tactic.BicategoryCoherence.LiftHom h] [Mathlib.Tactic.BicategoryCoherence.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 Mathlib.Tactic.BicategoryCoherence.bicategoricalIsoComp {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {f : a ⟶ b} {g : a ⟶ b} {h : a ⟶ b} {i : a ⟶ b} [Mathlib.Tactic.BicategoryCoherence.LiftHom g] [Mathlib.Tactic.BicategoryCoherence.LiftHom h] [Mathlib.Tactic.BicategoryCoherence.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.

@[simp]

theorem Mathlib.Tactic.BicategoryCoherence.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) : Mathlib.Tactic.BicategoryCoherence.bicategoricalComp η θ = CategoryTheory.CategoryStruct.comp η θ

def Mathlib.Tactic.BicategoryCoherence.exception {α : Type} (g : Lean.MVarId) (msg : Lean.MessageData) : Lean.MetaM α

Helper function for throwing exceptions.

def Mathlib.Tactic.BicategoryCoherence.exception' (msg : Lean.MessageData) : Lean.Elab.Tactic.TacticM Unit

Helper function for throwing exceptions with respect to the main goal.

def Mathlib.Tactic.BicategoryCoherence.mkLiftMap₂LiftExpr (e : Lean.Expr) : Lean.Elab.TermElabM Lean.Expr

Auxiliary definition for bicategorical_coherence.

def Mathlib.Tactic.BicategoryCoherence.bicategory_coherence (g : Lean.MVarId) : Lean.Elab.TermElabM Unit

Coherence tactic for bicategories.

def Mathlib.Tactic.BicategoryCoherence.tacticBicategory_coherence : Lean.ParserDescr

Coherence tactic for bicategories. Use pure_coherence instead, which is a frontend to this one.

def Mathlib.Tactic.BicategoryCoherence.whisker_simps : Lean.ParserDescr

Simp lemmas for rewriting a 2-morphism into a normal form.

theorem Mathlib.Tactic.BicategoryCoherence.assoc_liftHom₂ {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {f : a ⟶ b} {g : a ⟶ b} {h : a ⟶ b} {i : a ⟶ b} [Mathlib.Tactic.BicategoryCoherence.LiftHom f] [Mathlib.Tactic.BicategoryCoherence.LiftHom g] [Mathlib.Tactic.BicategoryCoherence.LiftHom h] (η : f ⟶ g) (θ : g ⟶ h) (ι : h ⟶ i) [Mathlib.Tactic.BicategoryCoherence.LiftHom₂ η] [Mathlib.Tactic.BicategoryCoherence.LiftHom₂ θ] : CategoryTheory.CategoryStruct.comp η (CategoryTheory.CategoryStruct.comp θ ι) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp η θ) ι

Auxiliary simp lemma for the coherence tactic: this move brackets to the left in order to expose a maximal prefix built out of unitors and associators.