Commit 2023-05-18 03:55 01d72c46

View on Github →

feat: port CategoryTheory.Bicategory.Free (#2482)

depends on: #2301

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Bicategory/Free.lean

added inductive CategoryTheory.FreeBicategory.Hom

added inductive CategoryTheory.FreeBicategory.Hom₂

added inductive CategoryTheory.FreeBicategory.Rel

added theorem CategoryTheory.FreeBicategory.comp_def

added def CategoryTheory.FreeBicategory.lift

added def CategoryTheory.FreeBicategory.liftHom

added theorem CategoryTheory.FreeBicategory.liftHom_comp

added theorem CategoryTheory.FreeBicategory.liftHom_id

added def CategoryTheory.FreeBicategory.liftHom₂

added theorem CategoryTheory.FreeBicategory.liftHom₂_congr

added theorem CategoryTheory.FreeBicategory.mk_associator_hom

added theorem CategoryTheory.FreeBicategory.mk_associator_inv

added theorem CategoryTheory.FreeBicategory.mk_id

added theorem CategoryTheory.FreeBicategory.mk_left_unitor_hom

added theorem CategoryTheory.FreeBicategory.mk_left_unitor_inv

added theorem CategoryTheory.FreeBicategory.mk_right_unitor_hom

added theorem CategoryTheory.FreeBicategory.mk_right_unitor_inv

added theorem CategoryTheory.FreeBicategory.mk_vcomp

added theorem CategoryTheory.FreeBicategory.mk_whisker_left

added theorem CategoryTheory.FreeBicategory.mk_whisker_right

added def CategoryTheory.FreeBicategory.of

added def CategoryTheory.FreeBicategory