Def CategoryTheory.FunctorToTypes.rightAdj

Modification history

2026-04-14 15:27
Mathlib/CategoryTheory/Monoidal/Closed/FunctorToTypes.lean
refactor(CategoryTheory): one-field structure morphisms in the category of types (#36613) …
Modified CategoryTheory.FunctorToTypes.rightAdjView on Github →
2024-09-23 14:47
Mathlib/CategoryTheory/Closed/FunctorToTypes.lean
feat(CategoryTheory): `MonoidalClosed` instance on functors to `Type` (#13710) …
Added CategoryTheory.FunctorToTypes.rightAdjView on Github →