Bicategories #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
In this file we define typeclass for bicategories.
A bicategory B consists of
- objects
a : B, - 1-morphisms
f : a ⟶ bbetween objectsa b : B, and - 2-morphisms
η : f ⟶ gbeween 1-morphismsf g : a ⟶ bbetween objectsa b : B.
We use u, v, and w as the universe variables for objects, 1-morphisms, and 2-morphisms,
respectively.
A typeclass for bicategories extends category_theory.category_struct typeclass. This means that
we have
- a composition
f ≫ g : a ⟶ cfor each 1-morphismsf : a ⟶ bandg : b ⟶ c, and - a identity
𝟙 a : a ⟶ afor each objecta : B.
For each object a b : B, the collection of 1-morphisms a ⟶ b has a category structure. The
2-morphisms in the bicategory are implemented as the morphisms in this family of categories.
The composition of 1-morphisms is in fact a object part of a functor
(a ⟶ b) ⥤ (b ⟶ c) ⥤ (a ⟶ c). The definition of bicategories in this file does not
require this functor directly. Instead, it requires the whiskering functions. For a 1-morphism
f : a ⟶ b and a 2-morphism η : g ⟶ h between 1-morphisms g h : b ⟶ c, there is a
2-morphism whisker_left f η : f ≫ g ⟶ f ≫ h. Similarly, for a 2-morphism η : f ⟶ g
between 1-morphisms f g : a ⟶ b and a 1-morphism f : b ⟶ c, there is a 2-morphism
whisker_right η h : f ≫ h ⟶ g ≫ h. These satisfy the exchange law
whisker_left f θ ≫ whisker_right η i = whisker_right η h ≫ whisker_left g θ,
which is required as an axiom in the definition here.
@[nolint, class]
- to_category_struct : category_theory.category_struct B
- hom_category : (Π (a b : B), category_theory.category (a ⟶ b)) . "apply_instance"
- whisker_left : Π {a b c : B} (f : a ⟶ b) {g h : b ⟶ c}, (g ⟶ h) → (f ≫ g ⟶ f ≫ h)
- whisker_right : Π {a b c : B} {f g : a ⟶ b}, (f ⟶ g) → Π (h : b ⟶ c), f ≫ h ⟶ g ≫ h
- associator : Π {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d), (f ≫ g) ≫ h ≅ f ≫ g ≫ h
- left_unitor : Π {a b : B} (f : a ⟶ b), 𝟙 a ≫ f ≅ f
- right_unitor : Π {a b : B} (f : a ⟶ b), f ≫ 𝟙 b ≅ f
- whisker_left_id' : (∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), category_theory.bicategory.whisker_left f (𝟙 g) = 𝟙 (f ≫ g)) . "obviously"
- whisker_left_comp' : (∀ {a b c : B} (f : a ⟶ b) {g h i : b ⟶ c} (η : g ⟶ h) (θ : h ⟶ i), category_theory.bicategory.whisker_left f (η ≫ θ) = category_theory.bicategory.whisker_left f η ≫ category_theory.bicategory.whisker_left f θ) . "obviously"
- id_whisker_left' : (∀ {a b : B} {f g : a ⟶ b} (η : f ⟶ g), category_theory.bicategory.whisker_left (𝟙 a) η = (category_theory.bicategory.left_unitor f).hom ≫ η ≫ (category_theory.bicategory.left_unitor g).inv) . "obviously"
- comp_whisker_left' : (∀ {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) {h h' : c ⟶ d} (η : h ⟶ h'), category_theory.bicategory.whisker_left (f ≫ g) η = (category_theory.bicategory.associator f g h).hom ≫ category_theory.bicategory.whisker_left f (category_theory.bicategory.whisker_left g η) ≫ (category_theory.bicategory.associator f g h').inv) . "obviously"
- id_whisker_right' : (∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), category_theory.bicategory.whisker_right (𝟙 f) g = 𝟙 (f ≫ g)) . "obviously"
- comp_whisker_right' : (∀ {a b c : B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h) (i : b ⟶ c), category_theory.bicategory.whisker_right (η ≫ θ) i = category_theory.bicategory.whisker_right η i ≫ category_theory.bicategory.whisker_right θ i) . "obviously"
- whisker_right_id' : (∀ {a b : B} {f g : a ⟶ b} (η : f ⟶ g), category_theory.bicategory.whisker_right η (𝟙 b) = (category_theory.bicategory.right_unitor f).hom ≫ η ≫ (category_theory.bicategory.right_unitor g).inv) . "obviously"
- whisker_right_comp' : (∀ {a b c d : B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) (h : c ⟶ d), category_theory.bicategory.whisker_right η (g ≫ h) = (category_theory.bicategory.associator f g h).inv ≫ category_theory.bicategory.whisker_right (category_theory.bicategory.whisker_right η g) h ≫ (category_theory.bicategory.associator f' g h).hom) . "obviously"
- whisker_assoc' : (∀ {a b c d : B} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g') (h : c ⟶ d), category_theory.bicategory.whisker_right (category_theory.bicategory.whisker_left f η) h = (category_theory.bicategory.associator f g h).hom ≫ category_theory.bicategory.whisker_left f (category_theory.bicategory.whisker_right η h) ≫ (category_theory.bicategory.associator f g' h).inv) . "obviously"
- whisker_exchange' : (∀ {a b c : B} {f g : a ⟶ b} {h i : b ⟶ c} (η : f ⟶ g) (θ : h ⟶ i), category_theory.bicategory.whisker_left f θ ≫ category_theory.bicategory.whisker_right η i = category_theory.bicategory.whisker_right η h ≫ category_theory.bicategory.whisker_left g θ) . "obviously"
- pentagon' : (∀ {a b c d e : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e), category_theory.bicategory.whisker_right (category_theory.bicategory.associator f g h).hom i ≫ (category_theory.bicategory.associator f (g ≫ h) i).hom ≫ category_theory.bicategory.whisker_left f (category_theory.bicategory.associator g h i).hom = (category_theory.bicategory.associator (f ≫ g) h i).hom ≫ (category_theory.bicategory.associator f g (h ≫ i)).hom) . "obviously"
- triangle' : (∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), (category_theory.bicategory.associator f (𝟙 b) g).hom ≫ category_theory.bicategory.whisker_left f (category_theory.bicategory.left_unitor g).hom = category_theory.bicategory.whisker_right (category_theory.bicategory.right_unitor f).hom g) . "obviously"
In a bicategory, we can compose the 1-morphisms f : a ⟶ b and g : b ⟶ c to obtain
a 1-morphism f ≫ g : a ⟶ c. This composition does not need to be strictly associative,
but there is a specified associator, α_ f g h : (f ≫ g) ≫ h ≅ f ≫ (g ≫ h).
There is an identity 1-morphism 𝟙 a : a ⟶ a, with specified left and right unitor
isomorphisms λ_ f : 𝟙 a ≫ f ≅ f and ρ_ f : f ≫ 𝟙 a ≅ f.
These associators and unitors satisfy the pentagon and triangle equations.
See https://ncatlab.org/nlab/show/bicategory.
Instances of this typeclass
Instances of other typeclasses for category_theory.bicategory
- category_theory.bicategory.has_sizeof_inst
Simp-normal form for 2-morphisms #
Rewriting involving associators and unitors could be very complicated. We try to ease this
complexity by putting carefully chosen simp lemmas that rewrite any 2-morphisms into simp-normal
form defined below. Rewriting into simp-normal form is also useful when applying (forthcoming)
coherence tactic.
The simp-normal form of 2-morphisms is defined to be an expression that has the minimal number of parentheses. More precisely,
- it is a composition of 2-morphisms like
η₁ ≫ η₂ ≫ η₃ ≫ η₄ ≫ η₅such that eachηᵢis either a structural 2-morphisms (2-morphisms made up only of identities, associators, unitors) or non-structural 2-morphisms, and - each non-structural 2-morphism in the composition is of the form
f₁ ◁ f₂ ◁ f₃ ◁ η ▷ f₄ ▷ f₅, where eachfᵢis a 1-morphism that is not the identity or a composite andηis a non-structural 2-morphisms that is also not the identity or a composite.
Note that f₁ ◁ f₂ ◁ f₃ ◁ η ▷ f₄ ▷ f₅ is actually f₁ ◁ (f₂ ◁ (f₃ ◁ ((η ▷ f₄) ▷ f₅))).
@[simp]
theorem
category_theory.bicategory.whisker_left_id
{B : Type u}
[self : category_theory.bicategory B]
{a b c : B}
(f : a ⟶ b)
(g : b ⟶ c) :
category_theory.bicategory.whisker_left f (𝟙 g) = 𝟙 (f ≫ g)
@[simp]
theorem
category_theory.bicategory.whisker_left_comp
{B : Type u}
[self : category_theory.bicategory B]
{a b c : B}
(f : a ⟶ b)
{g h i : b ⟶ c}
(η : g ⟶ h)
(θ : h ⟶ i) :
@[simp]
theorem
category_theory.bicategory.id_whisker_left
{B : Type u}
[self : category_theory.bicategory B]
{a b : B}
{f g : a ⟶ b}
(η : f ⟶ g) :
@[simp]
theorem
category_theory.bicategory.comp_whisker_left
{B : Type u}
[self : category_theory.bicategory B]
{a b c d : B}
(f : a ⟶ b)
(g : b ⟶ c)
{h h' : c ⟶ d}
(η : h ⟶ h') :
@[simp]
theorem
category_theory.bicategory.id_whisker_right
{B : Type u}
[self : category_theory.bicategory B]
{a b c : B}
(f : a ⟶ b)
(g : b ⟶ c) :
category_theory.bicategory.whisker_right (𝟙 f) g = 𝟙 (f ≫ g)
@[simp]
theorem
category_theory.bicategory.comp_whisker_right
{B : Type u}
[self : category_theory.bicategory B]
{a b c : B}
{f g h : a ⟶ b}
(η : f ⟶ g)
(θ : g ⟶ h)
(i : b ⟶ c) :
@[simp]
theorem
category_theory.bicategory.whisker_right_id
{B : Type u}
[self : category_theory.bicategory B]
{a b : B}
{f g : a ⟶ b}
(η : f ⟶ g) :
@[simp]
theorem
category_theory.bicategory.whisker_right_comp
{B : Type u}
[self : category_theory.bicategory B]
{a b c d : B}
{f f' : a ⟶ b}
(η : f ⟶ f')
(g : b ⟶ c)
(h : c ⟶ d) :
@[simp]
theorem
category_theory.bicategory.whisker_assoc
{B : Type u}
[self : category_theory.bicategory B]
{a b c d : B}
(f : a ⟶ b)
{g g' : b ⟶ c}
(η : g ⟶ g')
(h : c ⟶ d) :
theorem
category_theory.bicategory.whisker_exchange
{B : Type u}
[self : category_theory.bicategory B]
{a b c : B}
{f g : a ⟶ b}
{h i : b ⟶ c}
(η : f ⟶ g)
(θ : h ⟶ i) :
@[simp]
theorem
category_theory.bicategory.pentagon
{B : Type u}
[self : category_theory.bicategory B]
{a b c d e : B}
(f : a ⟶ b)
(g : b ⟶ c)
(h : c ⟶ d)
(i : d ⟶ e) :
category_theory.bicategory.whisker_right (category_theory.bicategory.associator f g h).hom i ≫ (category_theory.bicategory.associator f (g ≫ h) i).hom ≫ category_theory.bicategory.whisker_left f (category_theory.bicategory.associator g h i).hom = (category_theory.bicategory.associator (f ≫ g) h i).hom ≫ (category_theory.bicategory.associator f g (h ≫ i)).hom
@[simp]
theorem
category_theory.bicategory.triangle
{B : Type u}
[self : category_theory.bicategory B]
{a b c : B}
(f : a ⟶ b)
(g : b ⟶ c) :
@[simp]
theorem
category_theory.bicategory.pentagon_assoc
{B : Type u}
[self : category_theory.bicategory B]
{a b c d e : B}
(f : a ⟶ b)
(g : b ⟶ c)
(h : c ⟶ d)
(i : d ⟶ e)
{X' : a ⟶ e}
(f' : f ≫ g ≫ h ≫ i ⟶ X') :
category_theory.bicategory.whisker_right (category_theory.bicategory.associator f g h).hom i ≫ (category_theory.bicategory.associator f (g ≫ h) i).hom ≫ category_theory.bicategory.whisker_left f (category_theory.bicategory.associator g h i).hom ≫ f' = (category_theory.bicategory.associator (f ≫ g) h i).hom ≫ (category_theory.bicategory.associator f g (h ≫ i)).hom ≫ f'
theorem
category_theory.bicategory.id_whisker_left_assoc
{B : Type u}
[self : category_theory.bicategory B]
{a b : B}
{f g : a ⟶ b}
(η : f ⟶ g)
{X' : a ⟶ b}
(f' : 𝟙 a ≫ g ⟶ X') :
category_theory.bicategory.whisker_left (𝟙 a) η ≫ f' = (category_theory.bicategory.left_unitor f).hom ≫ η ≫ (category_theory.bicategory.left_unitor g).inv ≫ f'
theorem
category_theory.bicategory.comp_whisker_left_assoc
{B : Type u}
[self : category_theory.bicategory B]
{a b c d : B}
(f : a ⟶ b)
(g : b ⟶ c)
{h h' : c ⟶ d}
(η : h ⟶ h')
{X' : a ⟶ d}
(f' : (f ≫ g) ≫ h' ⟶ X') :
category_theory.bicategory.whisker_left (f ≫ g) η ≫ f' = (category_theory.bicategory.associator f g h).hom ≫ category_theory.bicategory.whisker_left f (category_theory.bicategory.whisker_left g η) ≫ (category_theory.bicategory.associator f g h').inv ≫ f'
theorem
category_theory.bicategory.comp_whisker_right_assoc
{B : Type u}
[self : category_theory.bicategory B]
{a b c : B}
{f g h : a ⟶ b}
(η : f ⟶ g)
(θ : g ⟶ h)
(i : b ⟶ c)
{X' : a ⟶ c}
(f' : h ≫ i ⟶ X') :
theorem
category_theory.bicategory.whisker_right_id_assoc
{B : Type u}
[self : category_theory.bicategory B]
{a b : B}
{f g : a ⟶ b}
(η : f ⟶ g)
{X' : a ⟶ b}
(f' : g ≫ 𝟙 b ⟶ X') :
theorem
category_theory.bicategory.whisker_right_comp_assoc
{B : Type u}
[self : category_theory.bicategory B]
{a b c d : B}
{f f' : a ⟶ b}
(η : f ⟶ f')
(g : b ⟶ c)
(h : c ⟶ d)
{X' : a ⟶ d}
(f'_1 : f' ≫ g ≫ h ⟶ X') :
category_theory.bicategory.whisker_right η (g ≫ h) ≫ f'_1 = (category_theory.bicategory.associator f g h).inv ≫ category_theory.bicategory.whisker_right (category_theory.bicategory.whisker_right η g) h ≫ (category_theory.bicategory.associator f' g h).hom ≫ f'_1
theorem
category_theory.bicategory.whisker_exchange_assoc
{B : Type u}
[self : category_theory.bicategory B]
{a b c : B}
{f g : a ⟶ b}
{h i : b ⟶ c}
(η : f ⟶ g)
(θ : h ⟶ i)
{X' : a ⟶ c}
(f' : g ≫ i ⟶ X') :
@[simp]
theorem
category_theory.bicategory.triangle_assoc
{B : Type u}
[self : category_theory.bicategory B]
{a b c : B}
(f : a ⟶ b)
(g : b ⟶ c)
{X' : a ⟶ c}
(f' : f ≫ g ⟶ X') :
theorem
category_theory.bicategory.whisker_left_comp_assoc
{B : Type u}
[self : category_theory.bicategory B]
{a b c : B}
(f : a ⟶ b)
{g h i : b ⟶ c}
(η : g ⟶ h)
(θ : h ⟶ i)
{X' : a ⟶ c}
(f' : f ≫ i ⟶ X') :
@[simp]
theorem
category_theory.bicategory.hom_inv_whisker_left_assoc
{B : Type u}
[category_theory.bicategory B]
{a b c : B}
(f : a ⟶ b)
{g h : b ⟶ c}
(η : g ≅ h)
{X' : a ⟶ c}
(f' : f ≫ g ⟶ X') :
@[simp]
theorem
category_theory.bicategory.hom_inv_whisker_left
{B : Type u}
[category_theory.bicategory B]
{a b c : B}
(f : a ⟶ b)
{g h : b ⟶ c}
(η : g ≅ h) :
@[simp]
theorem
category_theory.bicategory.hom_inv_whisker_right
{B : Type u}
[category_theory.bicategory B]
{a b c : B}
{f g : a ⟶ b}
(η : f ≅ g)
(h : b ⟶ c) :
@[simp]
theorem
category_theory.bicategory.hom_inv_whisker_right_assoc
{B : Type u}
[category_theory.bicategory B]
{a b c : B}
{f g : a ⟶ b}
(η : f ≅ g)
(h : b ⟶ c)
{X' : a ⟶ c}
(f' : f ≫ h ⟶ X') :
@[simp]
theorem
category_theory.bicategory.inv_hom_whisker_left_assoc
{B : Type u}
[category_theory.bicategory B]
{a b c : B}
(f : a ⟶ b)
{g h : b ⟶ c}
(η : g ≅ h)
{X' : a ⟶ c}
(f' : f ≫ h ⟶ X') :
@[simp]
theorem
category_theory.bicategory.inv_hom_whisker_left
{B : Type u}
[category_theory.bicategory B]
{a b c : B}
(f : a ⟶ b)
{g h : b ⟶ c}
(η : g ≅ h) :
@[simp]
theorem
category_theory.bicategory.inv_hom_whisker_right_assoc
{B : Type u}
[category_theory.bicategory B]
{a b c : B}
{f g : a ⟶ b}
(η : f ≅ g)
(h : b ⟶ c)
{X' : a ⟶ c}
(f' : g ≫ h ⟶ X') :
@[simp]
theorem
category_theory.bicategory.inv_hom_whisker_right
{B : Type u}
[category_theory.bicategory B]
{a b c : B}
{f g : a ⟶ b}
(η : f ≅ g)
(h : b ⟶ c) :
@[simp]
theorem
category_theory.bicategory.whisker_left_iso_inv
{B : Type u}
[category_theory.bicategory B]
{a b c : B}
(f : a ⟶ b)
{g h : b ⟶ c}
(η : g ≅ h) :
@[simp]
theorem
category_theory.bicategory.whisker_left_iso_hom
{B : Type u}
[category_theory.bicategory B]
{a b c : B}
(f : a ⟶ b)
{g h : b ⟶ c}
(η : g ≅ h) :
def
category_theory.bicategory.whisker_left_iso
{B : Type u}
[category_theory.bicategory B]
{a b c : B}
(f : a ⟶ b)
{g h : b ⟶ c}
(η : g ≅ h) :
The left whiskering of a 2-isomorphism is a 2-isomorphism.
Equations
- category_theory.bicategory.whisker_left_iso f η = {hom := category_theory.bicategory.whisker_left f η.hom, inv := category_theory.bicategory.whisker_left f η.inv, hom_inv_id' := _, inv_hom_id' := _}
@[protected, instance]
def
category_theory.bicategory.whisker_left_is_iso
{B : Type u}
[category_theory.bicategory B]
{a b c : B}
(f : a ⟶ b)
{g h : b ⟶ c}
(η : g ⟶ h)
[category_theory.is_iso η] :
@[simp]
theorem
category_theory.bicategory.inv_whisker_left
{B : Type u}
[category_theory.bicategory B]
{a b c : B}
(f : a ⟶ b)
{g h : b ⟶ c}
(η : g ⟶ h)
[category_theory.is_iso η] :
def
category_theory.bicategory.whisker_right_iso
{B : Type u}
[category_theory.bicategory B]
{a b c : B}
{f g : a ⟶ b}
(η : f ≅ g)
(h : b ⟶ c) :
The right whiskering of a 2-isomorphism is a 2-isomorphism.
Equations
- category_theory.bicategory.whisker_right_iso η h = {hom := category_theory.bicategory.whisker_right η.hom h, inv := category_theory.bicategory.whisker_right η.inv h, hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
category_theory.bicategory.whisker_right_iso_hom
{B : Type u}
[category_theory.bicategory B]
{a b c : B}
{f g : a ⟶ b}
(η : f ≅ g)
(h : b ⟶ c) :
@[simp]
theorem
category_theory.bicategory.whisker_right_iso_inv
{B : Type u}
[category_theory.bicategory B]
{a b c : B}
{f g : a ⟶ b}
(η : f ≅ g)
(h : b ⟶ c) :
@[protected, instance]
def
category_theory.bicategory.whisker_right_is_iso
{B : Type u}
[category_theory.bicategory B]
{a b c : B}
{f g : a ⟶ b}
(η : f ⟶ g)
(h : b ⟶ c)
[category_theory.is_iso η] :
@[simp]
theorem
category_theory.bicategory.inv_whisker_right
{B : Type u}
[category_theory.bicategory B]
{a b c : B}
{f g : a ⟶ b}
(η : f ⟶ g)
(h : b ⟶ c)
[category_theory.is_iso η] :
@[simp]
theorem
category_theory.bicategory.pentagon_inv_assoc
{B : Type u}
[category_theory.bicategory B]
{a b c d e : B}
(f : a ⟶ b)
(g : b ⟶ c)
(h : c ⟶ d)
(i : d ⟶ e)
{X' : a ⟶ e}
(f' : ((f ≫ g) ≫ h) ≫ i ⟶ X') :
category_theory.bicategory.whisker_left f (category_theory.bicategory.associator g h i).inv ≫ (category_theory.bicategory.associator f (g ≫ h) i).inv ≫ category_theory.bicategory.whisker_right (category_theory.bicategory.associator f g h).inv i ≫ f' = (category_theory.bicategory.associator f g (h ≫ i)).inv ≫ (category_theory.bicategory.associator (f ≫ g) h i).inv ≫ f'
@[simp]
theorem
category_theory.bicategory.pentagon_inv
{B : Type u}
[category_theory.bicategory B]
{a b c d e : B}
(f : a ⟶ b)
(g : b ⟶ c)
(h : c ⟶ d)
(i : d ⟶ e) :
category_theory.bicategory.whisker_left f (category_theory.bicategory.associator g h i).inv ≫ (category_theory.bicategory.associator f (g ≫ h) i).inv ≫ category_theory.bicategory.whisker_right (category_theory.bicategory.associator f g h).inv i = (category_theory.bicategory.associator f g (h ≫ i)).inv ≫ (category_theory.bicategory.associator (f ≫ g) h i).inv
@[simp]
theorem
category_theory.bicategory.pentagon_inv_inv_hom_hom_inv
{B : Type u}
[category_theory.bicategory B]
{a b c d e : B}
(f : a ⟶ b)
(g : b ⟶ c)
(h : c ⟶ d)
(i : d ⟶ e) :
(category_theory.bicategory.associator f (g ≫ h) i).inv ≫ category_theory.bicategory.whisker_right (category_theory.bicategory.associator f g h).inv i ≫ (category_theory.bicategory.associator (f ≫ g) h i).hom = category_theory.bicategory.whisker_left f (category_theory.bicategory.associator g h i).hom ≫ (category_theory.bicategory.associator f g (h ≫ i)).inv
@[simp]
theorem
category_theory.bicategory.pentagon_inv_inv_hom_hom_inv_assoc
{B : Type u}
[category_theory.bicategory B]
{a b c d e : B}
(f : a ⟶ b)
(g : b ⟶ c)
(h : c ⟶ d)
(i : d ⟶ e)
{X' : a ⟶ e}
(f' : (f ≫ g) ≫ h ≫ i ⟶ X') :
(category_theory.bicategory.associator f (g ≫ h) i).inv ≫ category_theory.bicategory.whisker_right (category_theory.bicategory.associator f g h).inv i ≫ (category_theory.bicategory.associator (f ≫ g) h i).hom ≫ f' = category_theory.bicategory.whisker_left f (category_theory.bicategory.associator g h i).hom ≫ (category_theory.bicategory.associator f g (h ≫ i)).inv ≫ f'
@[simp]
theorem
category_theory.bicategory.pentagon_inv_hom_hom_hom_inv_assoc
{B : Type u}
[category_theory.bicategory B]
{a b c d e : B}
(f : a ⟶ b)
(g : b ⟶ c)
(h : c ⟶ d)
(i : d ⟶ e)
{X' : a ⟶ e}
(f' : f ≫ (g ≫ h) ≫ i ⟶ X') :
(category_theory.bicategory.associator (f ≫ g) h i).inv ≫ category_theory.bicategory.whisker_right (category_theory.bicategory.associator f g h).hom i ≫ (category_theory.bicategory.associator f (g ≫ h) i).hom ≫ f' = (category_theory.bicategory.associator f g (h ≫ i)).hom ≫ category_theory.bicategory.whisker_left f (category_theory.bicategory.associator g h i).inv ≫ f'
@[simp]
theorem
category_theory.bicategory.pentagon_inv_hom_hom_hom_inv
{B : Type u}
[category_theory.bicategory B]
{a b c d e : B}
(f : a ⟶ b)
(g : b ⟶ c)
(h : c ⟶ d)
(i : d ⟶ e) :
(category_theory.bicategory.associator (f ≫ g) h i).inv ≫ category_theory.bicategory.whisker_right (category_theory.bicategory.associator f g h).hom i ≫ (category_theory.bicategory.associator f (g ≫ h) i).hom = (category_theory.bicategory.associator f g (h ≫ i)).hom ≫ category_theory.bicategory.whisker_left f (category_theory.bicategory.associator g h i).inv
@[simp]
theorem
category_theory.bicategory.pentagon_hom_inv_inv_inv_inv_assoc
{B : Type u}
[category_theory.bicategory B]
{a b c d e : B}
(f : a ⟶ b)
(g : b ⟶ c)
(h : c ⟶ d)
(i : d ⟶ e)
{X' : a ⟶ e}
(f' : ((f ≫ g) ≫ h) ≫ i ⟶ X') :
category_theory.bicategory.whisker_left f (category_theory.bicategory.associator g h i).hom ≫ (category_theory.bicategory.associator f g (h ≫ i)).inv ≫ (category_theory.bicategory.associator (f ≫ g) h i).inv ≫ f' = (category_theory.bicategory.associator f (g ≫ h) i).inv ≫ category_theory.bicategory.whisker_right (category_theory.bicategory.associator f g h).inv i ≫ f'
@[simp]
theorem
category_theory.bicategory.pentagon_hom_inv_inv_inv_inv
{B : Type u}
[category_theory.bicategory B]
{a b c d e : B}
(f : a ⟶ b)
(g : b ⟶ c)
(h : c ⟶ d)
(i : d ⟶ e) :
category_theory.bicategory.whisker_left f (category_theory.bicategory.associator g h i).hom ≫ (category_theory.bicategory.associator f g (h ≫ i)).inv ≫ (category_theory.bicategory.associator (f ≫ g) h i).inv = (category_theory.bicategory.associator f (g ≫ h) i).inv ≫ category_theory.bicategory.whisker_right (category_theory.bicategory.associator f g h).inv i
@[simp]
theorem
category_theory.bicategory.pentagon_hom_hom_inv_hom_hom
{B : Type u}
[category_theory.bicategory B]
{a b c d e : B}
(f : a ⟶ b)
(g : b ⟶ c)
(h : c ⟶ d)
(i : d ⟶ e) :
(category_theory.bicategory.associator (f ≫ g) h i).hom ≫ (category_theory.bicategory.associator f g (h ≫ i)).hom ≫ category_theory.bicategory.whisker_left f (category_theory.bicategory.associator g h i).inv = category_theory.bicategory.whisker_right (category_theory.bicategory.associator f g h).hom i ≫ (category_theory.bicategory.associator f (g ≫ h) i).hom
@[simp]
theorem
category_theory.bicategory.pentagon_hom_hom_inv_hom_hom_assoc
{B : Type u}
[category_theory.bicategory B]
{a b c d e : B}
(f : a ⟶ b)
(g : b ⟶ c)
(h : c ⟶ d)
(i : d ⟶ e)
{X' : a ⟶ e}
(f' : f ≫ (g ≫ h) ≫ i ⟶ X') :
(category_theory.bicategory.associator (f ≫ g) h i).hom ≫ (category_theory.bicategory.associator f g (h ≫ i)).hom ≫ category_theory.bicategory.whisker_left f (category_theory.bicategory.associator g h i).inv ≫ f' = category_theory.bicategory.whisker_right (category_theory.bicategory.associator f g h).hom i ≫ (category_theory.bicategory.associator f (g ≫ h) i).hom ≫ f'
@[simp]
theorem
category_theory.bicategory.pentagon_hom_inv_inv_inv_hom_assoc
{B : Type u}
[category_theory.bicategory B]
{a b c d e : B}
(f : a ⟶ b)
(g : b ⟶ c)
(h : c ⟶ d)
(i : d ⟶ e)
{X' : a ⟶ e}
(f' : (f ≫ g ≫ h) ≫ i ⟶ X') :
(category_theory.bicategory.associator f g (h ≫ i)).hom ≫ category_theory.bicategory.whisker_left f (category_theory.bicategory.associator g h i).inv ≫ (category_theory.bicategory.associator f (g ≫ h) i).inv ≫ f' = (category_theory.bicategory.associator (f ≫ g) h i).inv ≫ category_theory.bicategory.whisker_right (category_theory.bicategory.associator f g h).hom i ≫ f'
@[simp]
theorem
category_theory.bicategory.pentagon_hom_inv_inv_inv_hom
{B : Type u}
[category_theory.bicategory B]
{a b c d e : B}
(f : a ⟶ b)
(g : b ⟶ c)
(h : c ⟶ d)
(i : d ⟶ e) :
(category_theory.bicategory.associator f g (h ≫ i)).hom ≫ category_theory.bicategory.whisker_left f (category_theory.bicategory.associator g h i).inv ≫ (category_theory.bicategory.associator f (g ≫ h) i).inv = (category_theory.bicategory.associator (f ≫ g) h i).inv ≫ category_theory.bicategory.whisker_right (category_theory.bicategory.associator f g h).hom i
@[simp]
theorem
category_theory.bicategory.pentagon_hom_hom_inv_inv_hom
{B : Type u}
[category_theory.bicategory B]
{a b c d e : B}
(f : a ⟶ b)
(g : b ⟶ c)
(h : c ⟶ d)
(i : d ⟶ e) :
(category_theory.bicategory.associator f (g ≫ h) i).hom ≫ category_theory.bicategory.whisker_left f (category_theory.bicategory.associator g h i).hom ≫ (category_theory.bicategory.associator f g (h ≫ i)).inv = category_theory.bicategory.whisker_right (category_theory.bicategory.associator f g h).inv i ≫ (category_theory.bicategory.associator (f ≫ g) h i).hom
@[simp]
theorem
category_theory.bicategory.pentagon_hom_hom_inv_inv_hom_assoc
{B : Type u}
[category_theory.bicategory B]
{a b c d e : B}
(f : a ⟶ b)
(g : b ⟶ c)
(h : c ⟶ d)
(i : d ⟶ e)
{X' : a ⟶ e}
(f' : (f ≫ g) ≫ h ≫ i ⟶ X') :
(category_theory.bicategory.associator f (g ≫ h) i).hom ≫ category_theory.bicategory.whisker_left f (category_theory.bicategory.associator g h i).hom ≫ (category_theory.bicategory.associator f g (h ≫ i)).inv ≫ f' = category_theory.bicategory.whisker_right (category_theory.bicategory.associator f g h).inv i ≫ (category_theory.bicategory.associator (f ≫ g) h i).hom ≫ f'
@[simp]
theorem
category_theory.bicategory.pentagon_inv_hom_hom_hom_hom_assoc
{B : Type u}
[category_theory.bicategory B]
{a b c d e : B}
(f : a ⟶ b)
(g : b ⟶ c)
(h : c ⟶ d)
(i : d ⟶ e)
{X' : a ⟶ e}
(f' : f ≫ g ≫ h ≫ i ⟶ X') :
category_theory.bicategory.whisker_right (category_theory.bicategory.associator f g h).inv i ≫ (category_theory.bicategory.associator (f ≫ g) h i).hom ≫ (category_theory.bicategory.associator f g (h ≫ i)).hom ≫ f' = (category_theory.bicategory.associator f (g ≫ h) i).hom ≫ category_theory.bicategory.whisker_left f (category_theory.bicategory.associator g h i).hom ≫ f'
@[simp]
theorem
category_theory.bicategory.pentagon_inv_hom_hom_hom_hom
{B : Type u}
[category_theory.bicategory B]
{a b c d e : B}
(f : a ⟶ b)
(g : b ⟶ c)
(h : c ⟶ d)
(i : d ⟶ e) :
category_theory.bicategory.whisker_right (category_theory.bicategory.associator f g h).inv i ≫ (category_theory.bicategory.associator (f ≫ g) h i).hom ≫ (category_theory.bicategory.associator f g (h ≫ i)).hom = (category_theory.bicategory.associator f (g ≫ h) i).hom ≫ category_theory.bicategory.whisker_left f (category_theory.bicategory.associator g h i).hom
@[simp]
theorem
category_theory.bicategory.pentagon_inv_inv_hom_inv_inv
{B : Type u}
[category_theory.bicategory B]
{a b c d e : B}
(f : a ⟶ b)
(g : b ⟶ c)
(h : c ⟶ d)
(i : d ⟶ e) :
(category_theory.bicategory.associator f g (h ≫ i)).inv ≫ (category_theory.bicategory.associator (f ≫ g) h i).inv ≫ category_theory.bicategory.whisker_right (category_theory.bicategory.associator f g h).hom i = category_theory.bicategory.whisker_left f (category_theory.bicategory.associator g h i).inv ≫ (category_theory.bicategory.associator f (g ≫ h) i).inv
@[simp]
theorem
category_theory.bicategory.pentagon_inv_inv_hom_inv_inv_assoc
{B : Type u}
[category_theory.bicategory B]
{a b c d e : B}
(f : a ⟶ b)
(g : b ⟶ c)
(h : c ⟶ d)
(i : d ⟶ e)
{X' : a ⟶ e}
(f' : (f ≫ g ≫ h) ≫ i ⟶ X') :
(category_theory.bicategory.associator f g (h ≫ i)).inv ≫ (category_theory.bicategory.associator (f ≫ g) h i).inv ≫ category_theory.bicategory.whisker_right (category_theory.bicategory.associator f g h).hom i ≫ f' = category_theory.bicategory.whisker_left f (category_theory.bicategory.associator g h i).inv ≫ (category_theory.bicategory.associator f (g ≫ h) i).inv ≫ f'
theorem
category_theory.bicategory.triangle_assoc_comp_left
{B : Type u}
[category_theory.bicategory B]
{a b c : B}
(f : a ⟶ b)
(g : b ⟶ c) :
@[simp]
theorem
category_theory.bicategory.triangle_assoc_comp_right_assoc
{B : Type u}
[category_theory.bicategory B]
{a b c : B}
(f : a ⟶ b)
(g : b ⟶ c)
{X' : a ⟶ c}
(f' : f ≫ g ⟶ X') :
@[simp]
theorem
category_theory.bicategory.triangle_assoc_comp_right
{B : Type u}
[category_theory.bicategory B]
{a b c : B}
(f : a ⟶ b)
(g : b ⟶ c) :
@[simp]
theorem
category_theory.bicategory.triangle_assoc_comp_right_inv_assoc
{B : Type u}
[category_theory.bicategory B]
{a b c : B}
(f : a ⟶ b)
(g : b ⟶ c)
{X' : a ⟶ c}
(f' : f ≫ 𝟙 b ≫ g ⟶ X') :
@[simp]
theorem
category_theory.bicategory.triangle_assoc_comp_right_inv
{B : Type u}
[category_theory.bicategory B]
{a b c : B}
(f : a ⟶ b)
(g : b ⟶ c) :
@[simp]
theorem
category_theory.bicategory.triangle_assoc_comp_left_inv
{B : Type u}
[category_theory.bicategory B]
{a b c : B}
(f : a ⟶ b)
(g : b ⟶ c) :
@[simp]
theorem
category_theory.bicategory.triangle_assoc_comp_left_inv_assoc
{B : Type u}
[category_theory.bicategory B]
{a b c : B}
(f : a ⟶ b)
(g : b ⟶ c)
{X' : a ⟶ c}
(f' : (f ≫ 𝟙 b) ≫ g ⟶ X') :
theorem
category_theory.bicategory.associator_naturality_left_assoc
{B : Type u}
[category_theory.bicategory B]
{a b c d : B}
{f f' : a ⟶ b}
(η : f ⟶ f')
(g : b ⟶ c)
(h : c ⟶ d)
{X' : a ⟶ d}
(f'_1 : f' ≫ g ≫ h ⟶ X') :
category_theory.bicategory.whisker_right (category_theory.bicategory.whisker_right η g) h ≫ (category_theory.bicategory.associator f' g h).hom ≫ f'_1 = (category_theory.bicategory.associator f g h).hom ≫ category_theory.bicategory.whisker_right η (g ≫ h) ≫ f'_1
theorem
category_theory.bicategory.associator_naturality_left
{B : Type u}
[category_theory.bicategory B]
{a b c d : B}
{f f' : a ⟶ b}
(η : f ⟶ f')
(g : b ⟶ c)
(h : c ⟶ d) :
theorem
category_theory.bicategory.associator_inv_naturality_left
{B : Type u}
[category_theory.bicategory B]
{a b c d : B}
{f f' : a ⟶ b}
(η : f ⟶ f')
(g : b ⟶ c)
(h : c ⟶ d) :
theorem
category_theory.bicategory.associator_inv_naturality_left_assoc
{B : Type u}
[category_theory.bicategory B]
{a b c d : B}
{f f' : a ⟶ b}
(η : f ⟶ f')
(g : b ⟶ c)
(h : c ⟶ d)
{X' : a ⟶ d}
(f'_1 : (f' ≫ g) ≫ h ⟶ X') :
category_theory.bicategory.whisker_right η (g ≫ h) ≫ (category_theory.bicategory.associator f' g h).inv ≫ f'_1 = (category_theory.bicategory.associator f g h).inv ≫ category_theory.bicategory.whisker_right (category_theory.bicategory.whisker_right η g) h ≫ f'_1
theorem
category_theory.bicategory.whisker_right_comp_symm
{B : Type u}
[category_theory.bicategory B]
{a b c d : B}
{f f' : a ⟶ b}
(η : f ⟶ f')
(g : b ⟶ c)
(h : c ⟶ d) :
theorem
category_theory.bicategory.whisker_right_comp_symm_assoc
{B : Type u}
[category_theory.bicategory B]
{a b c d : B}
{f f' : a ⟶ b}
(η : f ⟶ f')
(g : b ⟶ c)
(h : c ⟶ d)
{X' : a ⟶ d}
(f'_1 : (f' ≫ g) ≫ h ⟶ X') :
category_theory.bicategory.whisker_right (category_theory.bicategory.whisker_right η g) h ≫ f'_1 = (category_theory.bicategory.associator f g h).hom ≫ category_theory.bicategory.whisker_right η (g ≫ h) ≫ (category_theory.bicategory.associator f' g h).inv ≫ f'_1
theorem
category_theory.bicategory.associator_naturality_middle
{B : Type u}
[category_theory.bicategory B]
{a b c d : B}
(f : a ⟶ b)
{g g' : b ⟶ c}
(η : g ⟶ g')
(h : c ⟶ d) :
theorem
category_theory.bicategory.associator_inv_naturality_middle
{B : Type u}
[category_theory.bicategory B]
{a b c d : B}
(f : a ⟶ b)
{g g' : b ⟶ c}
(η : g ⟶ g')
(h : c ⟶ d) :
theorem
category_theory.bicategory.whisker_assoc_symm
{B : Type u}
[category_theory.bicategory B]
{a b c d : B}
(f : a ⟶ b)
{g g' : b ⟶ c}
(η : g ⟶ g')
(h : c ⟶ d) :
theorem
category_theory.bicategory.associator_naturality_right
{B : Type u}
[category_theory.bicategory B]
{a b c d : B}
(f : a ⟶ b)
(g : b ⟶ c)
{h h' : c ⟶ d}
(η : h ⟶ h') :
theorem
category_theory.bicategory.associator_naturality_right_assoc
{B : Type u}
[category_theory.bicategory B]
{a b c d : B}
(f : a ⟶ b)
(g : b ⟶ c)
{h h' : c ⟶ d}
(η : h ⟶ h')
{X' : a ⟶ d}
(f' : f ≫ g ≫ h' ⟶ X') :
category_theory.bicategory.whisker_left (f ≫ g) η ≫ (category_theory.bicategory.associator f g h').hom ≫ f' = (category_theory.bicategory.associator f g h).hom ≫ category_theory.bicategory.whisker_left f (category_theory.bicategory.whisker_left g η) ≫ f'
theorem
category_theory.bicategory.associator_inv_naturality_right
{B : Type u}
[category_theory.bicategory B]
{a b c d : B}
(f : a ⟶ b)
(g : b ⟶ c)
{h h' : c ⟶ d}
(η : h ⟶ h') :
theorem
category_theory.bicategory.associator_inv_naturality_right_assoc
{B : Type u}
[category_theory.bicategory B]
{a b c d : B}
(f : a ⟶ b)
(g : b ⟶ c)
{h h' : c ⟶ d}
(η : h ⟶ h')
{X' : a ⟶ d}
(f' : (f ≫ g) ≫ h' ⟶ X') :
category_theory.bicategory.whisker_left f (category_theory.bicategory.whisker_left g η) ≫ (category_theory.bicategory.associator f g h').inv ≫ f' = (category_theory.bicategory.associator f g h).inv ≫ category_theory.bicategory.whisker_left (f ≫ g) η ≫ f'
theorem
category_theory.bicategory.comp_whisker_left_symm_assoc
{B : Type u}
[category_theory.bicategory B]
{a b c d : B}
(f : a ⟶ b)
(g : b ⟶ c)
{h h' : c ⟶ d}
(η : h ⟶ h')
{X' : a ⟶ d}
(f' : f ≫ g ≫ h' ⟶ X') :
category_theory.bicategory.whisker_left f (category_theory.bicategory.whisker_left g η) ≫ f' = (category_theory.bicategory.associator f g h).inv ≫ category_theory.bicategory.whisker_left (f ≫ g) η ≫ (category_theory.bicategory.associator f g h').hom ≫ f'
theorem
category_theory.bicategory.comp_whisker_left_symm
{B : Type u}
[category_theory.bicategory B]
{a b c d : B}
(f : a ⟶ b)
(g : b ⟶ c)
{h h' : c ⟶ d}
(η : h ⟶ h') :
theorem
category_theory.bicategory.left_unitor_naturality_assoc
{B : Type u}
[category_theory.bicategory B]
{a b : B}
{f g : a ⟶ b}
(η : f ⟶ g)
{X' : a ⟶ b}
(f' : g ⟶ X') :
category_theory.bicategory.whisker_left (𝟙 a) η ≫ (category_theory.bicategory.left_unitor g).hom ≫ f' = (category_theory.bicategory.left_unitor f).hom ≫ η ≫ f'
theorem
category_theory.bicategory.left_unitor_naturality
{B : Type u}
[category_theory.bicategory B]
{a b : B}
{f g : a ⟶ b}
(η : f ⟶ g) :
theorem
category_theory.bicategory.left_unitor_inv_naturality_assoc
{B : Type u}
[category_theory.bicategory B]
{a b : B}
{f g : a ⟶ b}
(η : f ⟶ g)
{X' : a ⟶ b}
(f' : 𝟙 a ≫ g ⟶ X') :
η ≫ (category_theory.bicategory.left_unitor g).inv ≫ f' = (category_theory.bicategory.left_unitor f).inv ≫ category_theory.bicategory.whisker_left (𝟙 a) η ≫ f'
theorem
category_theory.bicategory.left_unitor_inv_naturality
{B : Type u}
[category_theory.bicategory B]
{a b : B}
{f g : a ⟶ b}
(η : f ⟶ g) :
theorem
category_theory.bicategory.id_whisker_left_symm
{B : Type u}
[category_theory.bicategory B]
{a b : B}
{f g : a ⟶ b}
(η : f ⟶ g) :
theorem
category_theory.bicategory.right_unitor_naturality_assoc
{B : Type u}
[category_theory.bicategory B]
{a b : B}
{f g : a ⟶ b}
(η : f ⟶ g)
{X' : a ⟶ b}
(f' : g ⟶ X') :
theorem
category_theory.bicategory.right_unitor_naturality
{B : Type u}
[category_theory.bicategory B]
{a b : B}
{f g : a ⟶ b}
(η : f ⟶ g) :
theorem
category_theory.bicategory.right_unitor_inv_naturality
{B : Type u}
[category_theory.bicategory B]
{a b : B}
{f g : a ⟶ b}
(η : f ⟶ g) :
theorem
category_theory.bicategory.right_unitor_inv_naturality_assoc
{B : Type u}
[category_theory.bicategory B]
{a b : B}
{f g : a ⟶ b}
(η : f ⟶ g)
{X' : a ⟶ b}
(f' : g ≫ 𝟙 b ⟶ X') :
theorem
category_theory.bicategory.whisker_right_id_symm
{B : Type u}
[category_theory.bicategory B]
{a b : B}
{f g : a ⟶ b}
(η : f ⟶ g) :
theorem
category_theory.bicategory.whisker_left_iff
{B : Type u}
[category_theory.bicategory B]
{a b : B}
{f g : a ⟶ b}
(η θ : f ⟶ g) :
category_theory.bicategory.whisker_left (𝟙 a) η = category_theory.bicategory.whisker_left (𝟙 a) θ ↔ η = θ
theorem
category_theory.bicategory.whisker_right_iff
{B : Type u}
[category_theory.bicategory B]
{a b : B}
{f g : a ⟶ b}
(η θ : f ⟶ g) :
category_theory.bicategory.whisker_right η (𝟙 b) = category_theory.bicategory.whisker_right θ (𝟙 b) ↔ η = θ
theorem
category_theory.bicategory.left_unitor_whisker_right_assoc
{B : Type u}
[category_theory.bicategory B]
{a b c : B}
(f : a ⟶ b)
(g : b ⟶ c)
{X' : a ⟶ c}
(f' : f ≫ g ⟶ X') :
category_theory.bicategory.whisker_right (category_theory.bicategory.left_unitor f).hom g ≫ f' = (category_theory.bicategory.associator (𝟙 a) f g).hom ≫ (category_theory.bicategory.left_unitor (f ≫ g)).hom ≫ f'
@[simp]
theorem
category_theory.bicategory.left_unitor_whisker_right
{B : Type u}
[category_theory.bicategory B]
{a b c : B}
(f : a ⟶ b)
(g : b ⟶ c) :
We state it as a simp lemma, which is regarded as an involved version of
id_whisker_right f g : 𝟙 f ▷ g = 𝟙 (f ≫ g).
theorem
category_theory.bicategory.left_unitor_inv_whisker_right_assoc
{B : Type u}
[category_theory.bicategory B]
{a b c : B}
(f : a ⟶ b)
(g : b ⟶ c)
{X' : a ⟶ c}
(f' : (𝟙 a ≫ f) ≫ g ⟶ X') :
category_theory.bicategory.whisker_right (category_theory.bicategory.left_unitor f).inv g ≫ f' = (category_theory.bicategory.left_unitor (f ≫ g)).inv ≫ (category_theory.bicategory.associator (𝟙 a) f g).inv ≫ f'
@[simp]
theorem
category_theory.bicategory.left_unitor_inv_whisker_right
{B : Type u}
[category_theory.bicategory B]
{a b c : B}
(f : a ⟶ b)
(g : b ⟶ c) :
theorem
category_theory.bicategory.whisker_left_right_unitor_assoc
{B : Type u}
[category_theory.bicategory B]
{a b c : B}
(f : a ⟶ b)
(g : b ⟶ c)
{X' : a ⟶ c}
(f' : f ≫ g ⟶ X') :
@[simp]
theorem
category_theory.bicategory.whisker_left_right_unitor
{B : Type u}
[category_theory.bicategory B]
{a b c : B}
(f : a ⟶ b)
(g : b ⟶ c) :
@[simp]
theorem
category_theory.bicategory.whisker_left_right_unitor_inv
{B : Type u}
[category_theory.bicategory B]
{a b c : B}
(f : a ⟶ b)
(g : b ⟶ c) :
theorem
category_theory.bicategory.whisker_left_right_unitor_inv_assoc
{B : Type u}
[category_theory.bicategory B]
{a b c : B}
(f : a ⟶ b)
(g : b ⟶ c)
{X' : a ⟶ c}
(f' : f ≫ g ≫ 𝟙 c ⟶ X') :
theorem
category_theory.bicategory.left_unitor_comp_assoc
{B : Type u}
[category_theory.bicategory B]
{a b c : B}
(f : a ⟶ b)
(g : b ⟶ c)
{X' : a ⟶ c}
(f' : f ≫ g ⟶ X') :
(category_theory.bicategory.left_unitor (f ≫ g)).hom ≫ f' = (category_theory.bicategory.associator (𝟙 a) f g).inv ≫ category_theory.bicategory.whisker_right (category_theory.bicategory.left_unitor f).hom g ≫ f'
theorem
category_theory.bicategory.left_unitor_comp
{B : Type u}
[category_theory.bicategory B]
{a b c : B}
(f : a ⟶ b)
(g : b ⟶ c) :
theorem
category_theory.bicategory.left_unitor_comp_inv_assoc
{B : Type u}
[category_theory.bicategory B]
{a b c : B}
(f : a ⟶ b)
(g : b ⟶ c)
{X' : a ⟶ c}
(f' : 𝟙 a ≫ f ≫ g ⟶ X') :
(category_theory.bicategory.left_unitor (f ≫ g)).inv ≫ f' = category_theory.bicategory.whisker_right (category_theory.bicategory.left_unitor f).inv g ≫ (category_theory.bicategory.associator (𝟙 a) f g).hom ≫ f'
theorem
category_theory.bicategory.left_unitor_comp_inv
{B : Type u}
[category_theory.bicategory B]
{a b c : B}
(f : a ⟶ b)
(g : b ⟶ c) :
theorem
category_theory.bicategory.right_unitor_comp_assoc
{B : Type u}
[category_theory.bicategory B]
{a b c : B}
(f : a ⟶ b)
(g : b ⟶ c)
{X' : a ⟶ c}
(f' : f ≫ g ⟶ X') :
theorem
category_theory.bicategory.right_unitor_comp
{B : Type u}
[category_theory.bicategory B]
{a b c : B}
(f : a ⟶ b)
(g : b ⟶ c) :
theorem
category_theory.bicategory.right_unitor_comp_inv_assoc
{B : Type u}
[category_theory.bicategory B]
{a b c : B}
(f : a ⟶ b)
(g : b ⟶ c)
{X' : a ⟶ c}
(f' : (f ≫ g) ≫ 𝟙 c ⟶ X') :
theorem
category_theory.bicategory.right_unitor_comp_inv
{B : Type u}
[category_theory.bicategory B]
{a b c : B}
(f : a ⟶ b)
(g : b ⟶ c) :
@[simp]
theorem
category_theory.bicategory.unitors_equal
{B : Type u}
[category_theory.bicategory B]
{a : B} :
@[simp]
theorem
category_theory.bicategory.unitors_inv_equal
{B : Type u}
[category_theory.bicategory B]
{a : B} :