Commit 2025-11-04 09:42 7622f001

View on Github →

feat(Bicategory/Opposites): add 1-cell opposite bicategory (#25901) This PR adds the 1-cell opposite bicategory, where only the 1-morphisms are reversed.

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Bicategory/Opposites.lean

added structure Bicategory.Opposite.Hom2

added def Bicategory.Opposite.op2

added theorem Bicategory.Opposite.op2_associator

added theorem Bicategory.Opposite.op2_associator_hom

added theorem Bicategory.Opposite.op2_associator_inv

added theorem Bicategory.Opposite.op2_comp

added theorem Bicategory.Opposite.op2_id

added theorem Bicategory.Opposite.op2_id_unbop

added theorem Bicategory.Opposite.op2_leftUnitor

added theorem Bicategory.Opposite.op2_leftUnitor_hom

added theorem Bicategory.Opposite.op2_leftUnitor_inv

added theorem Bicategory.Opposite.op2_rightUnitor

added theorem Bicategory.Opposite.op2_rightUnitor_hom

added theorem Bicategory.Opposite.op2_rightUnitor_inv

added theorem Bicategory.Opposite.op2_unop2

added theorem Bicategory.Opposite.op2_whiskerLeft

added theorem Bicategory.Opposite.op2_whiskerRight

added def Bicategory.Opposite.opFunctor

added theorem Bicategory.Opposite.unop2_comp

added theorem Bicategory.Opposite.unop2_id

added theorem Bicategory.Opposite.unop2_id_bop

added theorem Bicategory.Opposite.unop2_op2

added def Bicategory.Opposite.unopFunctor

added theorem CategoryTheory.Iso.unop2_op2

Modified Mathlib/CategoryTheory/Opposites.lean

added theorem CategoryTheory.op_comp_assoc

added theorem CategoryTheory.op_comp_unop

added theorem CategoryTheory.unop_comp_assoc