Def CategoryTheory.MorphismProperty.Over.mapComp

Modification history

2026-01-14 14:01
Mathlib/CategoryTheory/MorphismProperty/OverAdjunction.lean
chore(CategoryTheory/MorphismProperty): improve def-eqs and add missing `MorphismProperty.Over.map` isomorphisms (#33931) …
Modified CategoryTheory.MorphismProperty.Over.mapCompView on Github →
2025-10-15 15:17
Mathlib/CategoryTheory/MorphismProperty/OverAdjunction.lean
refactor: weaken HasPullbacks to HasPullback in MorphismProperty.OverAdjuction (#29810) …
Modified CategoryTheory.MorphismProperty.Over.mapCompView 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.mapCompView on Github →