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.
Is there a name for the process of generating a new category from some arbitrary category by keeping the objects the same but identifying all the morphisms between the same objects? "Thinning" maybe?
It's changing base of enrichment, from to . Notice there is a canonical arrow from the first to the latter, which sends in and everything else in , and you can figure out what it does on arrows. Then the change of base along this functor is what you're after.
Terminologically though, I don't now
I think this is usually called the "preorder collapse" of a cateory, since the result is a preorder.
It just came to me that @sarahzrf likes to call -enriched categories (= preorders) depleted categories. So another term would be depletion.
(Or rather, Ω-enriched, if you don't assume excluded middle)
So how would you perform a change of base to constructively?
Matteo Capucci said:
It's changing base of enrichment, from to . Notice there is a canonical arrow from the first to the latter, which sends in and everything else in , and you can figure out what it does on arrows. Then the change of base along this functor is what you're after.
I've never seen it this way, but it's so neat!
Jacques Carette said:
So how would you perform a change of base to constructively?
If you have quotients, propositionally truncate. If you're working in E-categories, change the setoids to make all parallel morphisms equivalent.
Ah, of course! And "change the setoids to make all parallel morphisms equivalent", if that done by changing the equivalence to be constantly , that sure feels like truncation too. Nice.
Question: where does the terminology E-category come from?
I read it once, but I really don't remember. If anything, I'd hope you were the one who knew! :wink:
Googling around to find it. From the mid-2010s, Palmgren assumes everyone knows what it is, and doesn't cite anything for the definition of E category.
Kinoshita explicitly talks about them in " Y. Kinoshita, A bicategorical analysis of E-categories, Math. Jpn. 47 (1) (1998) 157–169."
So it seems that Dybjer called them E-Categories in his talk at MSCS 98, but the paper "Normalization and the Yoneda embedding" is actually about P-categories, which is E-categories where the equivalence relation is taken to be partial.
Of course, the use of E-category theory goes back to Aczel in his (unpublished) Galois project and development in LEGO. Credited by Huet and Saibi (who popularized it by using it in Coq.
So I guess someone should ask Dybjer.
"E-category" :clap: is :clap: a :clap: bad :clap: name
Why would anyone insist on using an initialism without specifying at least once what the initial stands for? I had assumed the E was the name of a (Grothendieck) topos, and that these were internal categories in that topos, which are canonically E-enriched; then is the subobject classifier, and depletion amounts to taking the support of a hom-object (the image of its unique morphism to the terminal object). But from your description, an E-category is a category equipped with some kind of equivalence relation? How was anyone supposed to guess that from the name?
I only use it because I know Jacques knows it and it's short. Usually, with less shared context, I'd probably say “setoid(-enriched) category” or similar.
Chad Nester said:
I think this is usually called the "preorder collapse" of a cateory, since the result is a preorder.
The nlab uses a small variation on this terminology: preorder reflection.
@[Mod] Morgan Rogers Yes, E-Category, even in its fancy-font version, like P-Category, are bad names. I think I'm ok with Setoid-enriched. [Though being ultra-precise and saying proof-relevant Setoid-enriched weak 1-category is perhaps a little much.]
[Mod] Morgan Rogers said:
"E-category" :clap: is :clap: a :clap: bad :clap: name
Why would anyone insist on using an initialism without specifying at least once what the initial stands for? I had assumed the E was the name of a (Grothendieck) topos, and that these were internal categories in that topos, which are canonically E-enriched; then is the subobject classifier, and depletion amounts to taking the support of a hom-object (the image of its unique morphism to the terminal object). But from your description, an E-category is a category equipped with some kind of equivalence relation? How was anyone supposed to guess that from the name?
I shared the confusion :laughing: I thought @James Wood's remark was about categories in a topos whose object of truth values in
I guess an E-cat is like an E-set plus morphisms? Where E-sets are sets with an equality predicate (E=equality), aka setoids aka Bishop sets
Equivalence predicate. Without J, I don't tend to call an equivalence relation an 'equality'.
J?
The computational J rule for identity elimination for identity types in Martin-Loef Type Theory. It's derivable from Yoneda, as per Martin Escardo.
Uh wow, I didn't know any of that
fun things to note: if we identify Ω with the subcategory of Set on subsingleton sets (this is [almost] precisely analogous to identifying Set with the subcategory of Cat on discrete categories—(-1)-Cat into 0-Cat instead of 0-Cat into 1-Cat), then the functor along which we change base of enrichment is in fact the left adjoint to the inclusion
more broadly:
...subterminals in C/A are exactly monomorphisms into A, and it turns out that reflecting a random object of C/A into a subterminal gives you an image factorization (the reflection unit is the other part of the factorization)—this is like saying that you're "truncating each fiber to a subsingleton so that you get an injection"
Matteo Capucci said:
Uh wow, I didn't know any of that
Type theorists, equality, &c. :laughter_tears:
Matteo Capucci said:
J?
Speaking of bad names...
I'm not sure you need the full induction principle (it might not make sense in other situations), but something analogous to the substitution principle.
Leibniz' characterization or something.
@sarahzrf I would love to formalize & integrate all of this into agda-categories. The formalizing is likely going to be straightforward, it is the really making use of it that is likely to be trickier. But it all 'feels' right.
i should take a look at agda-categories one of these days :thinking: