Mathlib Changelog
v4
Changelog
About
Github
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