Commit 2023-07-07 04:14 c6660d9a

View on Github →

feat: port CategoryTheory.Adjunction.Lifting (#4414)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Adjunction/Lifting.lean

added def CategoryTheory.LiftAdjoint.counitCoequalises

added def CategoryTheory.LiftAdjoint.otherMap