mathlib
bcd61b1d - feat(algebra/category): provide right adjoint instances for forget (#8235)

Commit

4 years ago

feat(algebra/category): provide right adjoint instances for forget (#8235) Also adds some universe variables since they weren't inferred sensibly.

Author

b-mehta

Parents