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.
feat(algebra/category): provide right adjoint instances for forget (#8235) Also adds some universe variables since they weren't inferred sensibly.