A coherence tactic for bicategories

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.

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.lean 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} (f : a ⟶ b) : Type (max u v)

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

• 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.

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible, instance 100]

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

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

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

• lift : LiftHom.lift f ⟶ LiftHom.lift g

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

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.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} {f g h i : a ⟶ b} [LiftHom f] [LiftHom g] [LiftHom h] (η : f ⟶ g) (θ : g ⟶ h) (ι : h ⟶ i) [LiftHom₂ η] [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.