agda
Pretopos
Since it looks like Setoids is not a topos, but instead a $\Pi W$-Pretopos, I was going to implement that (i.e. Pretopos and variants). My thinking is that I should put the definitions into Categories.Topos.Pre.
My reasoning is that Topos is the eventual goal and uniting concept (so a decent place to look). Of course, there's the counter-argument that Pretopos is 'more fundamental' and thus should be at the top level. I'm not convinced, as that would mean too many thing would be forced to the top level.
So this issue is to ask about opinions as to where to put this. @HuStmpHrrr @sstucki @TOTBWF @Taneb .
I vote for Categories.Topos.Pre or even Categories.Topos.Pretopos.
There are a lot of concepts X where X is a category with some extra structure. Sometimes that's explicit (e.g. monoidal category, cartesian category, bicategory, etc.) sometimes it's not (e.g. for topoi). In the library, some have associated top-level modules others don't. Maybe we ought to think about whether there's a rule of thumb for adding such top-level modules. I think if there's a sufficient body of theory for a given concept (like monoidal categories or bicategories) it makes sense to have a separate top-level module for that "theory". Topoi probably meet that criterion. But that's not quite how the library is organized now.
Also, I'd personally put monads and adjunctions under functors (rather than at the top level).
We do want the word Pretopos to show up. So maybe indeed the longer form is a good idea.
In a radical redo of CT, I'd agree that monads and adjunctions should go under functors... but I'm a little wary of being quite that radical right now. But I'm not dismissing it entirely as option.
I like Categories.Topos.Pretopos, as it is nice and discoverable, and also serves as a nice folder structure for various riffs on pretopoi, IE: Categories.Topos.Pretopos.Heyting.
On a related note, I've looked into doing this before and there are a lot of moving parts. Perhaps we should start a github project and make a bunch of issues for each of these, so that we can distribute the work.
I agree with what other people have said here. In particular, I like the idea of a Categories.Topos.Pretopos.X heirarchy
