Commit 2025-11-17 02:04 4a5073f8

View on Github →

feat(CategoryTheory/MorphismProperty): generalize to CategoryStructs (#31632) This generalizes some parts of MorphismProperty that only use the data underlying a Cateogory (i.e. everything in the file not mentioning isomorphisms or functors, although arguably functors should only use CategoryStructs also...). This will be useful for bicategories and stacks.

Estimated changes

Modified Mathlib/CategoryTheory/MorphismProperty/Basic.lean

modified theorem CategoryTheory.MorphismProperty.le_def

modified def CategoryTheory.MorphismProperty.prod

modified theorem CategoryTheory.MorphismProperty.top_eq

modified def CategoryTheory.MorphismProperty