Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-05-28 08:49
32f27227
View on Github →
feat: port/CategoryTheory.Bicategory.Coherence (
#4062
)
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/CategoryTheory/Bicategory/Coherence.lean
added
def
CategoryTheory.FreeBicategory.inclusion
added
def
CategoryTheory.FreeBicategory.inclusionMapCompAux
added
def
CategoryTheory.FreeBicategory.inclusionPath
added
def
CategoryTheory.FreeBicategory.inclusionPathAux
added
def
CategoryTheory.FreeBicategory.normalize
added
def
CategoryTheory.FreeBicategory.normalizeAux
added
theorem
CategoryTheory.FreeBicategory.normalizeAux_congr
added
theorem
CategoryTheory.FreeBicategory.normalizeAux_nil_comp
added
def
CategoryTheory.FreeBicategory.normalizeEquiv
added
def
CategoryTheory.FreeBicategory.normalizeIso
added
def
CategoryTheory.FreeBicategory.normalizeUnitIso
added
theorem
CategoryTheory.FreeBicategory.normalize_naturality
added
def
CategoryTheory.FreeBicategory.preinclusion
added
theorem
CategoryTheory.FreeBicategory.preinclusion_map₂
added
theorem
CategoryTheory.FreeBicategory.preinclusion_obj