# mathlibdocumentation

category_theory.bicategory.coherence

# The coherence theorem for bicategories #

In this file, we prove the coherence theorem for bicategories, stated in the following form: the free bicategory over any quiver is locally thin.

The proof is almost the same as the proof of the coherence theorem for monoidal categories that has been previously formalized in mathlib, which is based on the proof described by Ilya Beylin and Peter Dybjer. The idea is to view a path on a quiver as a normal form of a 1-morphism in the free bicategory on the same quiver. A normalization procedure is then described by normalize : pseudofunctor (free_bicategory B) (locally_discrete (paths B)), which is a pseudofunctor from the free bicategory to the locally discrete bicategory on the path category. It turns out that this pseudofunctor is locally an equivalence of categories, and the coherence theorem follows immediately from this fact.

## Main statements #

• locally_thin : the free bicategory is locally thin, that is, there is at most one 2-morphism between two fixed 1-morphisms.

## References #

@[simp]

Auxiliary definition for inclusion_path.

Equations
def category_theory.free_bicategory.inclusion_path {B : Type u} [quiver B] (a b : B) :

The discrete category on the paths includes into the category of 1-morphisms in the free bicategory.

Equations

The inclusion from the locally discrete bicategory on the path category into the free bicategory as a prelax functor. This will be promoted to a pseudofunctor after proving the coherence theorem. See inclusion.

Equations
@[simp]
theorem category_theory.free_bicategory.preinclusion_obj {B : Type u} [quiver B] (a : B) :
@[simp]
theorem category_theory.free_bicategory.preinclusion_map₂ {B : Type u} [quiver B] {a b : B} (f g : category_theory.discrete b)) (η : f g) :
@[simp]
def category_theory.free_bicategory.normalize_aux {B : Type u} [quiver B] {a b c : B} :
b

The normalization of the composition of p : path a b and f : hom b c. p will eventually be taken to be nil and we then get the normalization of f alone, but the auxiliary p is necessary for Lean to accept the definition of normalize_iso and the whisker_left case of normalize_aux_congr and normalize_naturality.

Equations
@[simp]
def category_theory.free_bicategory.normalize_iso {B : Type u} [quiver B] {a b c : B} (p : b)  :

A 2-isomorphism between a partially-normalized 1-morphism in the free bicategory to the fully-normalized 1-morphism.

Equations
theorem category_theory.free_bicategory.normalize_aux_congr {B : Type u} [quiver B] {a b c : B} (p : b) {f g : c} (η : f g) :

Given a 2-morphism between f and g in the free bicategory, we have the equality normalize_aux p f = normalize_aux p g.

theorem category_theory.free_bicategory.normalize_naturality {B : Type u} [quiver B] {a b c : B} (p : b) {f g : c} (η : f g) :

The 2-isomorphism normalize_iso p f is natural in f.

@[simp]

The normalization pseudofunctor for the free bicategory on a quiver B.

Equations

Auxiliary definition for normalize_equiv.

Equations
def category_theory.free_bicategory.normalize_equiv {B : Type u} [quiver B] (a b : B) :

Normalization as an equivalence of categories.

Equations
@[protected, instance]

The coherence theorem for bicategories.

def category_theory.free_bicategory.inclusion_map_comp_aux {B : Type u} [quiver B] {a b c : B} (f : b) (g : c) :
({as := f} {as := g})

Auxiliary definition for inclusion.

Equations

The inclusion pseudofunctor from the locally discrete bicategory on the path category into the free bicategory.

Equations