Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-29 07:35 1084cee9

View on Github →

feat(category_theory/bicategory/coherence): prove the coherence theorem for bicategories (#12155)

Estimated changes

Created src/category_theory/bicategory/coherence.lean

added def category_theory.free_bicategory.inclusion

added def category_theory.free_bicategory.inclusion_map_comp_aux

added def category_theory.free_bicategory.inclusion_path

added def category_theory.free_bicategory.inclusion_path_aux

added def category_theory.free_bicategory.normalize

added def category_theory.free_bicategory.normalize_aux

added theorem category_theory.free_bicategory.normalize_aux_congr

added theorem category_theory.free_bicategory.normalize_aux_nil_comp

added def category_theory.free_bicategory.normalize_equiv

added def category_theory.free_bicategory.normalize_iso

added theorem category_theory.free_bicategory.normalize_naturality

added def category_theory.free_bicategory.normalize_unit_iso

added def category_theory.free_bicategory.preinclusion

Modified src/category_theory/bicategory/free.lean

modified theorem category_theory.free_bicategory.comp_def

modified theorem category_theory.free_bicategory.id_def

Modified src/category_theory/bicategory/locally_discrete.lean

Modified src/category_theory/eq_to_hom.lean

added theorem category_theory.dcongr_arg