Theorem CategoryTheory.MorphismProperty.Over.map_comp

Modification history

2025-10-15 15:17

Mathlib/CategoryTheory/MorphismProperty/OverAdjunction.lean

refactor: weaken HasPullbacks to HasPullback in MorphismProperty.OverAdjuction (#29810) …

Modified CategoryTheory.MorphismProperty.Over.map_comp View on Github →

2024-11-27 11:40

Mathlib/CategoryTheory/MorphismProperty/OverAdjunction.lean

feat(CategoryTheory): pushforward pullback adjunction for `P.Over Q X` (#19271)

Added CategoryTheory.MorphismProperty.Over.map_comp View on Github →