Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2022-03-14 09:29
cd001b2d
View on Github →
feat(category_theory/bicategory/free): define free bicategories (
#11998
)
Estimated changes
Created
src/category_theory/bicategory/free.lean
added
theorem
category_theory.free_bicategory.comp_def
added
inductive
category_theory.free_bicategory.hom
added
inductive
category_theory.free_bicategory.hom₂
added
theorem
category_theory.free_bicategory.id_def
added
def
category_theory.free_bicategory.lift
added
def
category_theory.free_bicategory.lift_hom
added
theorem
category_theory.free_bicategory.lift_hom_comp
added
theorem
category_theory.free_bicategory.lift_hom_id
added
def
category_theory.free_bicategory.lift_hom₂
added
theorem
category_theory.free_bicategory.lift_hom₂_congr
added
theorem
category_theory.free_bicategory.mk_associator_hom
added
theorem
category_theory.free_bicategory.mk_associator_inv
added
theorem
category_theory.free_bicategory.mk_id
added
theorem
category_theory.free_bicategory.mk_left_unitor_hom
added
theorem
category_theory.free_bicategory.mk_left_unitor_inv
added
theorem
category_theory.free_bicategory.mk_right_unitor_hom
added
theorem
category_theory.free_bicategory.mk_right_unitor_inv
added
theorem
category_theory.free_bicategory.mk_vcomp
added
theorem
category_theory.free_bicategory.mk_whisker_left
added
theorem
category_theory.free_bicategory.mk_whisker_right
added
def
category_theory.free_bicategory.of
added
inductive
category_theory.free_bicategory.rel
added
def
category_theory.free_bicategory