Where to organize the 'with K' part of the categories library? about agda-categories HOT 7 CLOSED

If we go with top-level WithK, I completely agree that it ought to be able to refer to anything outside, but not the other way around. And indeed, re-exports are possible.

This might not fully solve the "what is Strict" issue, but at least it'll be clear that everything under the WithK hierarchy are strongly truncated.

from agda-categories.

Interesting question.

I don't like the idea of mixing with/without K. (I wonder why it is done like this in the stdlib.)

Having a separate top-level WithK module seems like a nice approach. I'd suggest that modules nested in WithK should be allowed to refer to those outside, but not vice-versa, so that without-K-modules are not accidentally tainted. And everything that can, should of course still go in the without-K-part of the hierarchy. One could then have a WithK version of some modules that re-export functionality from outside (e.g. the weak Grothendieck construction) and add extra proofs/constructions (e.g. the strict Grothendieck construction).

from agda-categories.

OK, I'll take care of this when I get some time (and after reworking #42).

from agda-categories.

if WithK is a separate hierarchy, wouldn't it be mostly empty?

from agda-categories.

The sparser the better! But I'm fine with that.

from agda-categories.

I don't like the idea of mixing with/without K. (I wonder why it is done like this in the stdlib.)

In the stdlib we adopted --without-K and --safe as defaults. As a consequence
--with-K and "unsafe" are considered outliers and even sometimes evidence of the
compiler not being advanced enough to recognize K-freeness or safety.
Correspondingly modules tainted by these options are left behind, like an afterthought.

from agda-categories.

Right now, there is no use of --with-K at all in the library. So there doesn't seem to be anything to 'do' for this particular issue (other than to decide how to organize things). And that decision seems to have been done: Use Categories/WithK as a hierarchy.

from agda-categories.