Commit 2023-02-07 04:16 8e132e27

View on Github →

feat: port CategoryTheory.Bicategory.Basic (#2126) Pretty straightforward except I don't know how to use aesop_cat in place of ext.

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Bicategory/Basic.lean

added theorem CategoryTheory.Bicategory.associator_inv_naturality_left

added theorem CategoryTheory.Bicategory.associator_inv_naturality_middle

added theorem CategoryTheory.Bicategory.associator_inv_naturality_right

added theorem CategoryTheory.Bicategory.associator_naturality_left

added theorem CategoryTheory.Bicategory.associator_naturality_middle

added theorem CategoryTheory.Bicategory.associator_naturality_right

added theorem CategoryTheory.Bicategory.comp_whiskerLeft_symm

added theorem CategoryTheory.Bicategory.hom_inv_whiskerLeft

added theorem CategoryTheory.Bicategory.hom_inv_whiskerRight

added theorem CategoryTheory.Bicategory.id_whiskerLeft_symm

added theorem CategoryTheory.Bicategory.inv_hom_whiskerLeft

added theorem CategoryTheory.Bicategory.inv_hom_whiskerRight

added theorem CategoryTheory.Bicategory.inv_whiskerLeft

added theorem CategoryTheory.Bicategory.inv_whiskerRight

added theorem CategoryTheory.Bicategory.leftUnitor_comp

added theorem CategoryTheory.Bicategory.leftUnitor_comp_inv

added theorem CategoryTheory.Bicategory.leftUnitor_inv_naturality

added theorem CategoryTheory.Bicategory.leftUnitor_inv_whiskerRight

added theorem CategoryTheory.Bicategory.leftUnitor_naturality

added theorem CategoryTheory.Bicategory.leftUnitor_whiskerRight

added theorem CategoryTheory.Bicategory.pentagon_hom_hom_inv_hom_hom

added theorem CategoryTheory.Bicategory.pentagon_hom_hom_inv_inv_hom

added theorem CategoryTheory.Bicategory.pentagon_hom_inv_inv_inv_hom

added theorem CategoryTheory.Bicategory.pentagon_hom_inv_inv_inv_inv

added theorem CategoryTheory.Bicategory.pentagon_inv

added theorem CategoryTheory.Bicategory.pentagon_inv_hom_hom_hom_hom

added theorem CategoryTheory.Bicategory.pentagon_inv_hom_hom_hom_inv

added theorem CategoryTheory.Bicategory.pentagon_inv_inv_hom_hom_inv

added theorem CategoryTheory.Bicategory.pentagon_inv_inv_hom_inv_inv

added theorem CategoryTheory.Bicategory.rightUnitor_comp

added theorem CategoryTheory.Bicategory.rightUnitor_comp_inv

added theorem CategoryTheory.Bicategory.rightUnitor_inv_naturality

added theorem CategoryTheory.Bicategory.rightUnitor_naturality

added theorem CategoryTheory.Bicategory.triangle_assoc_comp_left

added theorem CategoryTheory.Bicategory.triangle_assoc_comp_left_inv

added theorem CategoryTheory.Bicategory.triangle_assoc_comp_right

added theorem CategoryTheory.Bicategory.triangle_assoc_comp_right_inv

added theorem CategoryTheory.Bicategory.unitors_equal

added theorem CategoryTheory.Bicategory.unitors_inv_equal

added def CategoryTheory.Bicategory.whiskerLeftIso

added theorem CategoryTheory.Bicategory.whiskerLeft_iff

added theorem CategoryTheory.Bicategory.whiskerLeft_rightUnitor

added theorem CategoryTheory.Bicategory.whiskerLeft_rightUnitor_inv

added def CategoryTheory.Bicategory.whiskerRightIso

added theorem CategoryTheory.Bicategory.whiskerRight_comp_symm

added theorem CategoryTheory.Bicategory.whiskerRight_id_symm

added theorem CategoryTheory.Bicategory.whiskerRight_iff

added theorem CategoryTheory.Bicategory.whisker_assoc_symm

Modified Mathlib/CategoryTheory/Category/Basic.lean