# Coherence tactic for bicategories #

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

source
@[reducible, inline]
abbrev Mathlib.Tactic.Bicategory.normalizeIsoComp {B : Type u} [CategoryTheory.Bicategory B] {a b c d : B} {p : a ⟶ b} {f : b ⟶ c} {g : c ⟶ d} {pf : a ⟶ c} {pfg : a ⟶ d} (η_f : CategoryTheory.CategoryStruct.comp p f ≅ pf) (η_g : CategoryTheory.CategoryStruct.comp pf g ≅ pfg) :
CategoryTheory.CategoryStruct.comp p (CategoryTheory.CategoryStruct.comp f g) ≅ pfg

The composition of the normalizing isomorphisms `η_f : p ≫ f ≅ pf` and `η_g : pf ≫ g ≅ pfg`.

Equations

- Mathlib.Tactic.Bicategory.normalizeIsoComp η_f η_g = (CategoryTheory.Bicategory.associator p f g).symm ≪≫ CategoryTheory.Bicategory.whiskerRightIso η_f g ≪≫ η_g

Instances For

source
theorem Mathlib.Tactic.Bicategory.naturality_associator {B : Type u} [CategoryTheory.Bicategory B] {a b c d e : B} {p : a ⟶ b} {f : b ⟶ c} {g : c ⟶ d} {h : d ⟶ e} {pf : a ⟶ c} {pfg : a ⟶ d} {pfgh : a ⟶ e} (η_f : CategoryTheory.CategoryStruct.comp p f ≅ pf) (η_g : CategoryTheory.CategoryStruct.comp pf g ≅ pfg) (η_h : CategoryTheory.CategoryStruct.comp pfg h ≅ pfgh) :
CategoryTheory.Bicategory.whiskerLeftIso p (CategoryTheory.Bicategory.associator f g h) ≪≫ normalizeIsoComp η_f (normalizeIsoComp η_g η_h) = normalizeIsoComp (normalizeIsoComp η_f η_g) η_h
source
theorem Mathlib.Tactic.Bicategory.naturality_leftUnitor {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} {p : a ⟶ b} {f : b ⟶ c} {pf : a ⟶ c} (η_f : CategoryTheory.CategoryStruct.comp p f ≅ pf) :
CategoryTheory.Bicategory.whiskerLeftIso p (CategoryTheory.Bicategory.leftUnitor f) ≪≫ η_f = normalizeIsoComp (CategoryTheory.Bicategory.rightUnitor p) η_f
source
theorem Mathlib.Tactic.Bicategory.naturality_rightUnitor {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} {p : a ⟶ b} {f : b ⟶ c} {pf : a ⟶ c} (η_f : CategoryTheory.CategoryStruct.comp p f ≅ pf) :
CategoryTheory.Bicategory.whiskerLeftIso p (CategoryTheory.Bicategory.rightUnitor f) ≪≫ η_f = normalizeIsoComp η_f (CategoryTheory.Bicategory.rightUnitor pf)
source
theorem Mathlib.Tactic.Bicategory.naturality_id {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} {p : a ⟶ b} {f : b ⟶ c} {pf : a ⟶ c} (η_f : CategoryTheory.CategoryStruct.comp p f ≅ pf) :
CategoryTheory.Bicategory.whiskerLeftIso p (CategoryTheory.Iso.refl f) ≪≫ η_f = η_f
source
theorem Mathlib.Tactic.Bicategory.naturality_comp {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} {p : a ⟶ b} {f g h : b ⟶ c} {pf : a ⟶ c} {η : f ≅ g} {θ : g ≅ h} (η_f : CategoryTheory.CategoryStruct.comp p f ≅ pf) (η_g : CategoryTheory.CategoryStruct.comp p g ≅ pf) (η_h : CategoryTheory.CategoryStruct.comp p h ≅ pf) (ih_η : CategoryTheory.Bicategory.whiskerLeftIso p η ≪≫ η_g = η_f) (ih_θ : CategoryTheory.Bicategory.whiskerLeftIso p θ ≪≫ η_h = η_g) :
CategoryTheory.Bicategory.whiskerLeftIso p (η ≪≫ θ) ≪≫ η_h = η_f
source
theorem Mathlib.Tactic.Bicategory.naturality_whiskerLeft {B : Type u} [CategoryTheory.Bicategory B] {a b c d : B} {p : a ⟶ b} {f : b ⟶ c} {g h : c ⟶ d} {pf : a ⟶ c} {pfg : a ⟶ d} {η : g ≅ h} (η_f : CategoryTheory.CategoryStruct.comp p f ≅ pf) (η_fg : CategoryTheory.CategoryStruct.comp pf g ≅ pfg) (η_fh : CategoryTheory.CategoryStruct.comp pf h ≅ pfg) (ih_η : CategoryTheory.Bicategory.whiskerLeftIso pf η ≪≫ η_fh = η_fg) :
CategoryTheory.Bicategory.whiskerLeftIso p (CategoryTheory.Bicategory.whiskerLeftIso f η) ≪≫ normalizeIsoComp η_f η_fh = normalizeIsoComp η_f η_fg
source
theorem Mathlib.Tactic.Bicategory.naturality_whiskerRight {B : Type u} [CategoryTheory.Bicategory B] {a b c d : B} {p : a ⟶ b} {f g : b ⟶ c} {h : c ⟶ d} {pf : a ⟶ c} {pfh : a ⟶ d} {η : f ≅ g} (η_f : CategoryTheory.CategoryStruct.comp p f ≅ pf) (η_g : CategoryTheory.CategoryStruct.comp p g ≅ pf) (η_fh : CategoryTheory.CategoryStruct.comp pf h ≅ pfh) (ih_η : CategoryTheory.Bicategory.whiskerLeftIso p η ≪≫ η_g = η_f) :
CategoryTheory.Bicategory.whiskerLeftIso p (CategoryTheory.Bicategory.whiskerRightIso η h) ≪≫ normalizeIsoComp η_g η_fh = normalizeIsoComp η_f η_fh
source
theorem Mathlib.Tactic.Bicategory.naturality_inv {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} {p : a ⟶ b} {f g : b ⟶ c} {pf : a ⟶ c} {η : f ≅ g} (η_f : CategoryTheory.CategoryStruct.comp p f ≅ pf) (η_g : CategoryTheory.CategoryStruct.comp p g ≅ pf) (ih : CategoryTheory.Bicategory.whiskerLeftIso p η ≪≫ η_g = η_f) :
CategoryTheory.Bicategory.whiskerLeftIso p η.symm ≪≫ η_f = η_g
source
instance Mathlib.Tactic.Bicategory.instMonadNormalizeNaturalityBicategoryM :
BicategoryLike.MonadNormalizeNaturality BicategoryM
Equations

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

source
theorem Mathlib.Tactic.Bicategory.of_normalize_eq {B : Type u} [CategoryTheory.Bicategory B] {a b : B} {f g f' : a ⟶ b} {η θ : f ≅ g} (η_f : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id a) f ≅ f') (η_g : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id a) g ≅ f') (h_η : CategoryTheory.Bicategory.whiskerLeftIso (CategoryTheory.CategoryStruct.id a) η ≪≫ η_g = η_f) (h_θ : CategoryTheory.Bicategory.whiskerLeftIso (CategoryTheory.CategoryStruct.id a) θ ≪≫ η_g = η_f) :
η = θ
source
theorem Mathlib.Tactic.Bicategory.mk_eq_of_naturality {B : Type u} [CategoryTheory.Bicategory B] {a b : B} {f g f' : a ⟶ b} {η θ : f ⟶ g} {η' θ' : f ≅ g} (η_f : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id a) f ≅ f') (η_g : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id a) g ≅ f') (Hη : η'.hom = η) (Hθ : θ'.hom = θ) (Hη' : CategoryTheory.Bicategory.whiskerLeftIso (CategoryTheory.CategoryStruct.id a) η' ≪≫ η_g = η_f) (Hθ' : CategoryTheory.Bicategory.whiskerLeftIso (CategoryTheory.CategoryStruct.id a) θ' ≪≫ η_g = η_f) :
η = θ
source
instance Mathlib.Tactic.Bicategory.instMkEqOfNaturalityBicategoryM :
BicategoryLike.MkEqOfNaturality BicategoryM
Equations

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

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

Close the goal of the form `η.hom = θ.hom`, where `η` and `θ` are 2-isomorphisms made up only of associators, unitors, and identities.

    example {B : Type} [Bicategory B] {a : B} :
      (λ_ (𝟙 a)).hom = (ρ_ (𝟙 a)).hom := by
      bicategory_coherence

Equations

- Mathlib.Tactic.Bicategory.pureCoherence mvarId = Mathlib.Tactic.BicategoryLike.pureCoherence Mathlib.Tactic.Bicategory.Context `bicategory mvarId

Instances For

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

Close the goal of the form `η.hom = θ.hom`, where `η` and `θ` are 2-isomorphisms made up only of associators, unitors, and identities.

    example {B : Type} [Bicategory B] {a : B} :
      (λ_ (𝟙 a)).hom = (ρ_ (𝟙 a)).hom := by
      bicategory_coherence

Equations

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

Instances For