Theorem CategoryTheory.monadicAdjointSquareLift

Modification history

2024-09-03 09:13

Mathlib/CategoryTheory/Adjunction/Lifting/Left.lean

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

Deleted CategoryTheory.monadicAdjointSquareLift View on Github →

2024-05-08 11:06

Mathlib/CategoryTheory/Adjunction/Lifting.lean

refactor(CategoryTheory): make Functor.IsEquivalence a Prop (#12462) …

Added CategoryTheory.monadicAdjointSquareLift View on Github →