Def OrderHom.equivalenceFunctor

Modification history

2025-07-31 19:24
Mathlib/CategoryTheory/Category/Preorder.lean
feat: basic translations between `X →o Y` and `X ⥤ Y` (#26415) …
Added OrderHom.equivalenceFunctorView on Github →