Commit 2026-03-12 20:50 f7071a90

View on Github →

feat(Bicategory/Yoneda): add the yoneda pseudofunctor (#30927)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Bicategory/Yoneda.lean

added def CategoryTheory.Bicategory.associatorNatIsoLeftCat

added def CategoryTheory.Bicategory.associatorNatIsoMiddleCat

added def CategoryTheory.Bicategory.associatorNatIsoRightCat

added def CategoryTheory.Bicategory.leftUnitorNatIsoCat

added def CategoryTheory.Bicategory.postcomposingCat

added def CategoryTheory.Bicategory.postcomposing₂

added def CategoryTheory.Bicategory.postcomp₂

added def CategoryTheory.Bicategory.precomposingCat

added def CategoryTheory.Bicategory.rightUnitorNatIsoCat

added def CategoryTheory.Bicategory.yoneda

added def CategoryTheory.Bicategory.yoneda₀

Modified Mathlib/Data/Opposite.lean

modified theorem Opposite.unop_injective