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

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

Instances

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

- Mathlib.Tactic.BicategoryCoherence.liftHomId = { lift := CategoryTheory.CategoryStruct.id (CategoryTheory.FreeBicategory.of.obj a) }

source
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)
Equations

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

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

- Mathlib.Tactic.BicategoryCoherence.liftHomOf f = { lift := CategoryTheory.FreeBicategory.of.map f }

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

Instances

source
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)
Equations

- Mathlib.Tactic.BicategoryCoherence.liftHom₂Id f = { lift := CategoryTheory.CategoryStruct.id (Mathlib.Tactic.BicategoryCoherence.LiftHom.lift f) }

source
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
Equations

- Mathlib.Tactic.BicategoryCoherence.liftHom₂LeftUnitorHom f = { lift := (CategoryTheory.Bicategory.leftUnitor (Mathlib.Tactic.BicategoryCoherence.LiftHom.lift f)).hom }

source
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
Equations

- Mathlib.Tactic.BicategoryCoherence.liftHom₂LeftUnitorInv f = { lift := (CategoryTheory.Bicategory.leftUnitor (Mathlib.Tactic.BicategoryCoherence.LiftHom.lift f)).inv }

source
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
Equations

- Mathlib.Tactic.BicategoryCoherence.liftHom₂RightUnitorHom f = { lift := (CategoryTheory.Bicategory.rightUnitor (Mathlib.Tactic.BicategoryCoherence.LiftHom.lift f)).hom }

source
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
Equations

- Mathlib.Tactic.BicategoryCoherence.liftHom₂RightUnitorInv f = { lift := (CategoryTheory.Bicategory.rightUnitor (Mathlib.Tactic.BicategoryCoherence.LiftHom.lift f)).inv }

source
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
Equations

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

source
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
Equations

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

source
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 η θ)
Equations

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

source
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 η)
Equations

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

source
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)
Equations

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

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

Helper function for throwing exceptions.

Equations

- Mathlib.Tactic.BicategoryCoherence.exception g msg = Lean.Meta.throwTacticEx `bicategorical_coherence g (some msg)

Instances For

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

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

Equations

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

Instances For

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

Auxiliary definition for `bicategorical_coherence`.

Equations

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

Instances For

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

Coherence tactic for bicategories.

Equations

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

Instances For

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

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

Equations

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

Instances For

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

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

Equations

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

Instances For

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