Normalization of 2-morphisms in bicategories #
This file provides the implementation of the normalization given in
Mathlib.Tactic.CategoryTheory.Coherence.Normalize. See this file for more details.
theorem
Mathlib.Tactic.Bicategory.evalComp_nil_nil
{B : Type u}
[CategoryTheory.Bicategory B]
{a b : B}
{f g h : a ⟶ b}
(α : f ≅ g)
(β : g ≅ h)
:
theorem
Mathlib.Tactic.Bicategory.evalComp_nil_cons
{B : Type u}
[CategoryTheory.Bicategory B]
{a b : B}
{f g h i j : a ⟶ b}
(α : f ≅ g)
(β : g ≅ h)
(η : h ⟶ i)
(ηs : i ⟶ j)
:
CategoryTheory.CategoryStruct.comp α.hom
(CategoryTheory.CategoryStruct.comp β.hom (CategoryTheory.CategoryStruct.comp η ηs)) = CategoryTheory.CategoryStruct.comp (α ≪≫ β).hom (CategoryTheory.CategoryStruct.comp η ηs)
theorem
Mathlib.Tactic.Bicategory.evalComp_cons
{B : Type u}
[CategoryTheory.Bicategory B]
{a b : B}
{f g h i j : a ⟶ b}
(α : f ≅ g)
(η : g ⟶ h)
{ηs : h ⟶ i}
{θ : i ⟶ j}
{ι : h ⟶ j}
(e_ι : CategoryTheory.CategoryStruct.comp ηs θ = ι)
:
theorem
Mathlib.Tactic.Bicategory.eval_comp
{B : Type u}
[CategoryTheory.Bicategory B]
{a b : B}
{f g h : a ⟶ b}
{η η' : f ⟶ g}
{θ θ' : g ⟶ h}
{ι : f ⟶ h}
(e_η : η = η')
(e_θ : θ = θ')
(e_ηθ : CategoryTheory.CategoryStruct.comp η' θ' = ι)
:
theorem
Mathlib.Tactic.Bicategory.eval_of
{B : Type u}
[CategoryTheory.Bicategory B]
{a b : B}
{f g : a ⟶ b}
(η : f ⟶ g)
:
theorem
Mathlib.Tactic.Bicategory.eval_monoidalComp
{B : Type u}
[CategoryTheory.Bicategory B]
{a b : B}
{f g h i : a ⟶ b}
{η η' : f ⟶ g}
{α : g ≅ h}
{θ θ' : h ⟶ i}
{αθ : g ⟶ i}
{ηαθ : f ⟶ i}
(e_η : η = η')
(e_θ : θ = θ')
(e_αθ : CategoryTheory.CategoryStruct.comp α.hom θ' = αθ)
(e_ηαθ : CategoryTheory.CategoryStruct.comp η' αθ = ηαθ)
:
CategoryTheory.CategoryStruct.comp η (CategoryTheory.CategoryStruct.comp α.hom θ) = ηαθ
theorem
Mathlib.Tactic.Bicategory.evalWhiskerLeft_nil
{B : Type u}
[CategoryTheory.Bicategory B]
{a b c : B}
(f : a ⟶ b)
{g h : b ⟶ c}
(α : g ≅ h)
:
(CategoryTheory.Bicategory.whiskerLeftIso f α).hom = (CategoryTheory.Bicategory.whiskerLeftIso f α).hom
theorem
Mathlib.Tactic.Bicategory.evalWhiskerLeft_of_cons
{B : Type u}
[CategoryTheory.Bicategory B]
{a b c : B}
{f : a ⟶ b}
{g h i j : b ⟶ c}
(α : g ≅ h)
(η : h ⟶ i)
{ηs : i ⟶ j}
{θ : CategoryTheory.CategoryStruct.comp f i ⟶ CategoryTheory.CategoryStruct.comp f j}
(e_θ : CategoryTheory.Bicategory.whiskerLeft f ηs = θ)
:
theorem
Mathlib.Tactic.Bicategory.evalWhiskerLeft_comp
{B : Type u}
[CategoryTheory.Bicategory B]
{a b c d : B}
{f : a ⟶ b}
{g : b ⟶ c}
{h i : c ⟶ d}
{η : h ⟶ i}
{η₁ : CategoryTheory.CategoryStruct.comp g h ⟶ CategoryTheory.CategoryStruct.comp g i}
{η₂ :
CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h) ⟶ CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g i)}
{η₃ :
CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h) ⟶ CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) i}
{η₄ :
CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h ⟶ CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) i}
(e_η₁ : CategoryTheory.Bicategory.whiskerLeft g η = η₁)
(e_η₂ : CategoryTheory.Bicategory.whiskerLeft f η₁ = η₂)
(e_η₃ : CategoryTheory.CategoryStruct.comp η₂ (CategoryTheory.Bicategory.associator f g i).inv = η₃)
(e_η₄ : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h).hom η₃ = η₄)
:
theorem
Mathlib.Tactic.Bicategory.evalWhiskerLeft_id
{B : Type u}
[CategoryTheory.Bicategory B]
{a b : B}
{f g : a ⟶ b}
{η : f ⟶ g}
{η₁ : f ⟶ CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id a) g}
{η₂ :
CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id a) f ⟶ CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id a) g}
(e_η₁ : CategoryTheory.CategoryStruct.comp η (CategoryTheory.Bicategory.leftUnitor g).inv = η₁)
(e_η₂ : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor f).hom η₁ = η₂)
:
theorem
Mathlib.Tactic.Bicategory.eval_whiskerLeft
{B : Type u}
[CategoryTheory.Bicategory B]
{a b c : B}
{f : a ⟶ b}
{g h : b ⟶ c}
{η η' : g ⟶ h}
{θ : CategoryTheory.CategoryStruct.comp f g ⟶ CategoryTheory.CategoryStruct.comp f h}
(e_η : η = η')
(e_θ : CategoryTheory.Bicategory.whiskerLeft f η' = θ)
:
theorem
Mathlib.Tactic.Bicategory.eval_whiskerRight
{B : Type u}
[CategoryTheory.Bicategory B]
{a b c : B}
{f g : a ⟶ b}
{h : b ⟶ c}
{η η' : f ⟶ g}
{θ : CategoryTheory.CategoryStruct.comp f h ⟶ CategoryTheory.CategoryStruct.comp g h}
(e_η : η = η')
(e_θ : CategoryTheory.Bicategory.whiskerRight η' h = θ)
:
theorem
Mathlib.Tactic.Bicategory.evalWhiskerRight_nil
{B : Type u}
[CategoryTheory.Bicategory B]
{a b c : B}
{f g : a ⟶ b}
(α : f ≅ g)
(h : b ⟶ c)
:
theorem
Mathlib.Tactic.Bicategory.evalWhiskerRightAux_of
{B : Type u}
[CategoryTheory.Bicategory B]
{a b c : B}
{f g : a ⟶ b}
(η : f ⟶ g)
(h : b ⟶ c)
:
CategoryTheory.Bicategory.whiskerRight η h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Iso.refl (CategoryTheory.CategoryStruct.comp f h)).hom
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight η h)
(CategoryTheory.Iso.refl (CategoryTheory.CategoryStruct.comp g h)).hom)
theorem
Mathlib.Tactic.Bicategory.evalWhiskerRight_cons_of_of
{B : Type u}
[CategoryTheory.Bicategory B]
{a b c : B}
{f g h i : a ⟶ b}
{j : b ⟶ c}
{α : f ≅ g}
{η : g ⟶ h}
{ηs : h ⟶ i}
{ηs₁ : CategoryTheory.CategoryStruct.comp h j ⟶ CategoryTheory.CategoryStruct.comp i j}
{η₁ : CategoryTheory.CategoryStruct.comp g j ⟶ CategoryTheory.CategoryStruct.comp h j}
{η₂ : CategoryTheory.CategoryStruct.comp g j ⟶ CategoryTheory.CategoryStruct.comp i j}
{η₃ : CategoryTheory.CategoryStruct.comp f j ⟶ CategoryTheory.CategoryStruct.comp i j}
(e_ηs₁ : CategoryTheory.Bicategory.whiskerRight ηs j = ηs₁)
(e_η₁ : CategoryTheory.Bicategory.whiskerRight η j = η₁)
(e_η₂ : CategoryTheory.CategoryStruct.comp η₁ ηs₁ = η₂)
(e_η₃ : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRightIso α j).hom η₂ = η₃)
:
theorem
Mathlib.Tactic.Bicategory.evalWhiskerRight_cons_whisker
{B : Type u}
[CategoryTheory.Bicategory B]
{a b c d : B}
{f : a ⟶ b}
{g : a ⟶ c}
{h i : b ⟶ c}
{j : a ⟶ c}
{k : c ⟶ d}
{α : g ≅ CategoryTheory.CategoryStruct.comp f h}
{η : h ⟶ i}
{ηs : CategoryTheory.CategoryStruct.comp f i ⟶ j}
{η₁ : CategoryTheory.CategoryStruct.comp h k ⟶ CategoryTheory.CategoryStruct.comp i k}
{η₂ :
CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp h k) ⟶ CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp i k)}
{ηs₁ :
CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f i) k ⟶ CategoryTheory.CategoryStruct.comp j k}
{ηs₂ :
CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp i k) ⟶ CategoryTheory.CategoryStruct.comp j k}
{η₃ :
CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp h k) ⟶ CategoryTheory.CategoryStruct.comp j k}
{η₄ :
CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f h) k ⟶ CategoryTheory.CategoryStruct.comp j k}
{η₅ : CategoryTheory.CategoryStruct.comp g k ⟶ CategoryTheory.CategoryStruct.comp j k}
(e_η₁ :
CategoryTheory.Bicategory.whiskerRight
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Iso.refl h).hom
(CategoryTheory.CategoryStruct.comp η (CategoryTheory.Iso.refl i).hom))
k = η₁)
(e_η₂ : CategoryTheory.Bicategory.whiskerLeft f η₁ = η₂)
(e_ηs₁ : CategoryTheory.Bicategory.whiskerRight ηs k = ηs₁)
(e_ηs₂ : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f i k).inv ηs₁ = ηs₂)
(e_η₃ : CategoryTheory.CategoryStruct.comp η₂ ηs₂ = η₃)
(e_η₄ : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f h k).hom η₃ = η₄)
(e_η₅ : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRightIso α k).hom η₄ = η₅)
:
theorem
Mathlib.Tactic.Bicategory.evalWhiskerRight_comp
{B : Type u}
[CategoryTheory.Bicategory B]
{a b c d : B}
{f f' : a ⟶ b}
{g : b ⟶ c}
{h : c ⟶ d}
{η : f ⟶ f'}
{η₁ : CategoryTheory.CategoryStruct.comp f g ⟶ CategoryTheory.CategoryStruct.comp f' g}
{η₂ :
CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h ⟶ CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f' g) h}
{η₃ :
CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h ⟶ CategoryTheory.CategoryStruct.comp f' (CategoryTheory.CategoryStruct.comp g h)}
{η₄ :
CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h) ⟶ CategoryTheory.CategoryStruct.comp f' (CategoryTheory.CategoryStruct.comp g h)}
(e_η₁ : CategoryTheory.Bicategory.whiskerRight η g = η₁)
(e_η₂ : CategoryTheory.Bicategory.whiskerRight η₁ h = η₂)
(e_η₃ : CategoryTheory.CategoryStruct.comp η₂ (CategoryTheory.Bicategory.associator f' g h).hom = η₃)
(e_η₄ : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h).inv η₃ = η₄)
:
theorem
Mathlib.Tactic.Bicategory.evalWhiskerRight_id
{B : Type u}
[CategoryTheory.Bicategory B]
{a b : B}
{f g : a ⟶ b}
{η : f ⟶ g}
{η₁ : f ⟶ CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.id b)}
{η₂ :
CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id b) ⟶ CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.id b)}
(e_η₁ : CategoryTheory.CategoryStruct.comp η (CategoryTheory.Bicategory.rightUnitor g).inv = η₁)
(e_η₂ : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor f).hom η₁ = η₂)
:
theorem
Mathlib.Tactic.Bicategory.eval_bicategoricalComp
{B : Type u}
[CategoryTheory.Bicategory B]
{a b : B}
{f g h i : a ⟶ b}
{η η' : f ⟶ g}
{α : g ≅ h}
{θ θ' : h ⟶ i}
{αθ : g ⟶ i}
{ηαθ : f ⟶ i}
(e_η : η = η')
(e_θ : θ = θ')
(e_αθ : CategoryTheory.CategoryStruct.comp α.hom θ' = αθ)
(e_ηαθ : CategoryTheory.CategoryStruct.comp η' αθ = ηαθ)
:
CategoryTheory.CategoryStruct.comp η (CategoryTheory.CategoryStruct.comp α.hom θ) = ηαθ
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.