While we're at it maybe we can standardize this notation too? I've seen that right angle all over the place and pointing in several different directions.

@TylerLawson Agreed! One concern I have however is that there doesn't seem to be a good description of that kind of enriched Grothendieck construction. Perhaps I should spend some time writing it down though. Dai Tamaki's construction doesn't seem to quite do the job.

I don't think one really needs abelian. For instance in this paper: arxiv.org/pdf/1105.3104v4.pdf one replaces commutative rings with presentable symmetric monoidal categories. Thus one might able to do something meaningful just working with presentable monoidal categories. But I agree that this connects to noncommutative algebraic geometry.

Here's a question: what conditions must one put on a subcategory so that quotienting by it yields a quotient-free category? I.e. what are the analogues of maximal ideals?

I feel like you should call these categories "entangled" or something. Or maybe "delicate."

Wanted to use the fundamental group of the circle, but then realized this required quotienting by homotopy equivalence.

I can't help wondering whether or not this is conflating the concept of a commutative diagram with the concept of implication in mathematical logic.