Def CategoryTheory.LiftRightAdjoint.unitEqualises

Modification history

2025-12-01 06:24

Mathlib/CategoryTheory/Adjunction/Lifting/Right.lean

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

Modified CategoryTheory.LiftRightAdjoint.unitEqualises View on Github →

2024-09-03 09:13

Mathlib/CategoryTheory/Adjunction/Lifting/Right.lean

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

Added CategoryTheory.LiftRightAdjoint.unitEqualises View on Github →