You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Shea Levy (Oct 25 2020 at 13:00):agda-categories defines -2-categories as a category where (quoting from their comments):
Is there a way to elegantly get -1-categories and 0-categories out of a definition like this? I can see -1 as being that |Hom x y| is contractible for all objects x y, which up to categorical equivalence means we either have no objects or one object with only the identity. But we'd want 0-categories to say that |Hom x x| is contractible and |Hom x y| is empty, which seems to break the pattern.
Jacques Carette (Oct 25 2020 at 16:28):We can get -1-categories and 0-categories more elegantly (in my mind) as having -1-categories be -2-category enriched (and similar one level up).
The "difficulty" with that definition is that you don't get that the category of -1-categories is equivalent to the poset of booleans! You need excluded middle to prove that. In fact, I'm pretty sure that it is equivalent to excluded middle, but I have not been able to prove it.
James Wood (Oct 25 2020 at 17:05):@Jacques Carette Are there proofs in the library that enrichment bumps up the number in the expected way? What form of equivalence would you be looking for?
Jacques Carette (Oct 25 2020 at 17:08):What do you mean by "bumps up the number in the expected way"? I'm pretty sure that the answer is 'no', as I'm pretty sure that such results are more meta-theoretical than what can be said in Agda itself. But it depends on exactly what you mean!
James Wood (Oct 25 2020 at 17:20):I mean that a -2 category-enriched category is a -1 category, a -1 category-enriched category is a 0 category, &c. I wouldn't expect a proof for all n, but surely each specific case can be done, right?
Jacques Carette (Oct 25 2020 at 17:41):You'd need a "by hand" definition of -1-category against which to compare. And that's where there's a rub: depending on the definition, it might not be provable. The usual definition of -1-category bakes in that things are either empty or contractible, which is not decidable without excluded middle. That's exactly where I got stuck!
Basically: I think there's a nice little paper here. Which I can't do on my own, as I need another brain to bounce ideas off of.
Shea Levy (Oct 25 2020 at 19:50):Jacques Carette said:
We can get -1-categories and 0-categories more elegantly (in my mind) as having -1-categories be -2-category enriched (and similar one level up).
The "difficulty" with that definition is that you don't get that the category of -1-categories is equivalent to the poset of booleans! You need excluded middle to prove that. In fact, I'm pretty sure that it is equivalent to excluded middle, but I have not been able to prove it.
So first your hom-objects are some connected set, then they're -2-categories, then they're -1 categories, then they're sets? What happens to the "contractible" part of the -2-cat defn?
Jacques Carette (Oct 26 2020 at 15:09):So first the object and homs are inhabited and connected - that gives you -2-categories. If you loosen 'inhabited' on objects, in theory you get -1-categories. Then you loosen connected on objects - that looks like Setoid; only Set if you squish things, which you might not really want to. Then you repeat one level up. This might not fully match the usual numbering though (it might be finer). At least, that's what I've been looking at. In theory, these are related, but the relation in published papers seems to use excluded middle and then choice, in non-trivial ways.
James Wood (Oct 26 2020 at 15:21):Why would you expect Setoid rather than Preorder (thin category)?
Shea Levy (Oct 26 2020 at 15:24):Yeah, when I tried this approach I got a preorder.
Jacques Carette (Oct 26 2020 at 16:00):Because I goofed, and was trying to do too many things too quickly, and wrote down junk in my message. Sigh.