Def CategoryTheory.Functor.mapComposableArrows

Modification history

2024-06-06 10:53
Mathlib/CategoryTheory/ComposableArrows.lean
feat: mapComposableArrows is essentially surjective for localization functors when there is a calculus of fractions (#13558) …
Modified CategoryTheory.Functor.mapComposableArrowsView on Github →
2023-11-03 20:42
Mathlib/CategoryTheory/ComposableArrows.lean
feat(CategoryTheory): inductive construction of composable arrows (#8146)
Added CategoryTheory.Functor.mapComposableArrowsView on Github →