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