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)
:
The composition of the normalizing isomorphisms η_f : p ≫ f ≅ pf and η_g : pf ≫ g ≅ pfg.
Equations
Instances For
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)
:
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)
:
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)
:
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)
:
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)
:
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)
:
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
Instances For
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