Def CategoryTheory.LiftLeftAdjoint.counitCoequalises

Modification history

2025-12-01 06:24

Mathlib/CategoryTheory/Adjunction/Lifting/Left.lean

refactor(Category Theory): change `RegularMono`/`Epi` from class to structure (#32154) …

Modified CategoryTheory.LiftLeftAdjoint.counitCoequalises View on Github →

2024-09-03 09:13

Mathlib/CategoryTheory/Adjunction/Lifting/Left.lean

feat(CategoryTheory/Adjunction): dualize adjoint lifting theorem (#16066) …

Added CategoryTheory.LiftLeftAdjoint.counitCoequalises View on Github →