Commit 2021-07-09 15:19 bcd61b1d

View on Github →

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

Estimated changes