Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-31 14:15 06a01971

View on Github →

feat(category_theory/bicategory/basic): define bicategories (#11079) This PR defines bicategories and gives basic lemmas.

Estimated changes

Created src/category_theory/bicategory/basic.lean

added theorem category_theory.bicategory.associator_conjugation_left

added theorem category_theory.bicategory.associator_conjugation_middle

added theorem category_theory.bicategory.associator_conjugation_right

added theorem category_theory.bicategory.associator_inv_conjugation_left

added theorem category_theory.bicategory.associator_inv_conjugation_middle

added theorem category_theory.bicategory.associator_inv_conjugation_right

added theorem category_theory.bicategory.associator_inv_naturality_left

added theorem category_theory.bicategory.associator_inv_naturality_middle

added theorem category_theory.bicategory.associator_inv_naturality_right

added theorem category_theory.bicategory.hom_inv_whisker_left

added theorem category_theory.bicategory.hom_inv_whisker_right

added theorem category_theory.bicategory.inv_hom_whisker_left

added theorem category_theory.bicategory.inv_hom_whisker_right

added theorem category_theory.bicategory.inv_whisker_left

added theorem category_theory.bicategory.inv_whisker_right

added theorem category_theory.bicategory.left_unitor_comp'

added theorem category_theory.bicategory.left_unitor_comp

added theorem category_theory.bicategory.left_unitor_comp_inv'

added theorem category_theory.bicategory.left_unitor_comp_inv

added theorem category_theory.bicategory.left_unitor_conjugation

added theorem category_theory.bicategory.left_unitor_inv_naturality

added theorem category_theory.bicategory.left_unitor_inv_whisker_right

added theorem category_theory.bicategory.left_unitor_whisker_right

added theorem category_theory.bicategory.pentagon_hom_hom_inv_hom_hom

added theorem category_theory.bicategory.pentagon_hom_hom_inv_inv_hom

added theorem category_theory.bicategory.pentagon_hom_inv_inv_inv_hom

added theorem category_theory.bicategory.pentagon_hom_inv_inv_inv_inv

added theorem category_theory.bicategory.pentagon_inv

added theorem category_theory.bicategory.pentagon_inv_hom_hom_hom_hom

added theorem category_theory.bicategory.pentagon_inv_hom_hom_hom_inv

added theorem category_theory.bicategory.pentagon_inv_inv_hom_hom_inv

added theorem category_theory.bicategory.pentagon_inv_inv_hom_inv_inv

added theorem category_theory.bicategory.right_unitor_comp

added theorem category_theory.bicategory.right_unitor_comp_inv

added theorem category_theory.bicategory.right_unitor_conjugation

added theorem category_theory.bicategory.right_unitor_inv_naturality

added theorem category_theory.bicategory.triangle_assoc_comp_left

added theorem category_theory.bicategory.triangle_assoc_comp_left_inv

added theorem category_theory.bicategory.triangle_assoc_comp_right

added theorem category_theory.bicategory.triangle_assoc_comp_right_inv

added theorem category_theory.bicategory.unitors_equal

added theorem category_theory.bicategory.unitors_inv_equal

added theorem category_theory.bicategory.whisker_left_iff

added def category_theory.bicategory.whisker_left_iso

added theorem category_theory.bicategory.whisker_left_right_unitor

added theorem category_theory.bicategory.whisker_left_right_unitor_inv

added theorem category_theory.bicategory.whisker_right_iff

added def category_theory.bicategory.whisker_right_iso