Mathlib Changelog
v3
Changelog
About
Github
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