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.

@[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

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

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

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)

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

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

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

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

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

@[instance_reducible]

instance Mathlib.Tactic.Bicategory.instMonadNormalizeNaturalityBicategoryM : BicategoryLike.MonadNormalizeNaturality BicategoryM

Equations

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

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) : η = θ

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) : η = θ

@[instance_reducible]

instance Mathlib.Tactic.Bicategory.instMkEqOfNaturalityBicategoryM : BicategoryLike.MkEqOfNaturality BicategoryM

Equations

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

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

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.