remove `levelOf` from `Category.Core` about agda-categories HOT 7 CLOSED

c.f. agda/agda-stdlib#829

from agda-categories.

f40c009

from agda-categories.

So the "problem" with this, is that agda-categories used to work fine on top of v1.0 and above the stdlib -- now it requires the master branch of post-v1.1. While I'm fine with dropping v1.0, requiring an unreleased library just for levelOfTerm seems like asking a lot.

from agda-categories.

hmm... i thought about that too. my thought was that since this library is not close to stable so following stdlib closer seems to speed up iteration. also I find levelOfTerm is quite useful because it becomes immediate what level the concept is in.

from agda-categories.

I guess we really (really!) don't want anything resembling an #ifdef anywhere in there, so we have to choose. And relying on a future v1.2 is probably ok. But we should not move further ahead than that!

from agda-categories.

ok fine. I hope it's the last new bit we need from the stdlib.

from agda-categories.

Or that we can sneak in whatever we need in time for 1.2.

from agda-categories.