bicategory tactic

This file provides bicategory tactic, which solves equations in a bicategory, where the two sides only differ by replacing strings of bicategory structural morphisms (that is, associators, unitors, and identities) with different strings of structural morphisms with the same source and target. In other words, bicategory solves equalities where both sides have the same string diagrams.

The core function for the bicategory tactic is provided in Mathlib.Tactic.CategoryTheory.Coherence.Basic. See this file for more details about the implementation.

def Mathlib.Tactic.Bicategory.bicategoryNf (mvarId : Lean.MVarId) : Lean.MetaM (List Lean.MVarId)

Normalize the both sides of an equality.

Equations

• Mathlib.Tactic.Bicategory.bicategoryNf mvarId = Mathlib.Tactic.BicategoryLike.normalForm Mathlib.Tactic.Bicategory.Context `bicategory mvarId

def Mathlib.Tactic.Bicategory.tacticBicategory_nf : Lean.ParserDescr

Normalize the both sides of an equality.

Equations

• Mathlib.Tactic.Bicategory.tacticBicategory_nf = Lean.ParserDescr.node `Mathlib.Tactic.Bicategory.tacticBicategory_nf 1024 (Lean.ParserDescr.nonReservedSymbol "bicategory_nf" false)

def Mathlib.Tactic.Bicategory.bicategory (mvarId : Lean.MVarId) : Lean.MetaM (List Lean.MVarId)

Use the coherence theorem for bicategories to solve equations in a bicategory, where the two sides only differ by replacing strings of bicategory structural morphisms (that is, associators, unitors, and identities) with different strings of structural morphisms with the same source and target.

That is, bicategory can handle goals of the form a ≫ f ≫ b ≫ g ≫ c = a' ≫ f ≫ b' ≫ g ≫ c' where a = a', b = b', and c = c' can be proved using bicategory_coherence.

Equations

• Mathlib.Tactic.Bicategory.bicategory mvarId = Mathlib.Tactic.BicategoryLike.main Mathlib.Tactic.Bicategory.Context `bicategory mvarId

def Mathlib.Tactic.Bicategory.tacticBicategory : Lean.ParserDescr

Use the coherence theorem for bicategories to solve equations in a bicategory, where the two sides only differ by replacing strings of bicategory structural morphisms (that is, associators, unitors, and identities) with different strings of structural morphisms with the same source and target.

That is, bicategory can handle goals of the form a ≫ f ≫ b ≫ g ≫ c = a' ≫ f ≫ b' ≫ g ≫ c' where a = a', b = b', and c = c' can be proved using bicategory_coherence.

Equations

• Mathlib.Tactic.Bicategory.tacticBicategory = Lean.ParserDescr.node `Mathlib.Tactic.Bicategory.tacticBicategory 1024 (Lean.ParserDescr.nonReservedSymbol "bicategory" false)