Category Theory
Zulip Server
Archive

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.


Stream: learning: questions

Topic: "Thinning" a category?


view this post on Zulip Shea Levy (Oct 14 2020 at 11:27):

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?

view this post on Zulip Matteo Capucci (he/him) (Oct 14 2020 at 11:30):

It's changing base of enrichment, from Set\mathbf{Set} to Bool={0<1}\mathbf{Bool} = \{0 < 1\}. Notice there is a canonical arrow from the first to the latter, which sends \varnothing in 00 and everything else in 11, and you can figure out what it does on arrows. Then the change of base along this functor is what you're after.

view this post on Zulip Matteo Capucci (he/him) (Oct 14 2020 at 11:31):

Terminologically though, I don't now

view this post on Zulip Chad Nester (Oct 14 2020 at 11:34):

I think this is usually called the "preorder collapse" of a cateory, since the result is a preorder.

view this post on Zulip Matteo Capucci (he/him) (Oct 14 2020 at 11:36):

It just came to me that @sarahzrf likes to call Bool\mathbf{Bool}-enriched categories (= preorders) depleted categories. So another term would be depletion.

view this post on Zulip James Wood (Oct 14 2020 at 12:12):

(Or rather, Ω-enriched, if you don't assume excluded middle)

view this post on Zulip Jacques Carette (Oct 14 2020 at 12:17):

So how would you perform a change of base to Ω\Omega constructively?

view this post on Zulip Fabrizio Genovese (Oct 14 2020 at 12:44):

Matteo Capucci said:

It's changing base of enrichment, from Set\mathbf{Set} to Bool={0<1}\mathbf{Bool} = \{0 < 1\}. Notice there is a canonical arrow from the first to the latter, which sends \varnothing in 00 and everything else in 11, 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!

view this post on Zulip James Wood (Oct 14 2020 at 12:46):

Jacques Carette said:

So how would you perform a change of base to Ω\Omega constructively?

If you have quotients, propositionally truncate. If you're working in E-categories, change the setoids to make all parallel morphisms equivalent.

view this post on Zulip Jacques Carette (Oct 14 2020 at 12:53):

Ah, of course! And "change the setoids to make all parallel morphisms equivalent", if that done by changing the equivalence to be constantly \top, that sure feels like truncation too. Nice.

Question: where does the terminology E-category come from?

view this post on Zulip James Wood (Oct 14 2020 at 12:57):

I read it once, but I really don't remember. If anything, I'd hope you were the one who knew! :wink:

view this post on Zulip Jacques Carette (Oct 14 2020 at 13:15):

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.

view this post on Zulip Jacques Carette (Oct 14 2020 at 13:19):

Kinoshita explicitly talks about them in " Y. Kinoshita, A bicategorical analysis of E-categories, Math. Jpn. 47 (1) (1998) 157–169."

view this post on Zulip Jacques Carette (Oct 14 2020 at 13:29):

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.

view this post on Zulip Jacques Carette (Oct 14 2020 at 13:34):

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.

view this post on Zulip Morgan Rogers (he/him) (Oct 14 2020 at 13:48):

"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 Ω\Omega 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?

view this post on Zulip James Wood (Oct 14 2020 at 14:06):

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.

view this post on Zulip Jens Hemelaer (Oct 14 2020 at 14:06):

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.

view this post on Zulip Jacques Carette (Oct 14 2020 at 14:14):

@[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.]

view this post on Zulip Matteo Capucci (he/him) (Oct 14 2020 at 14:16):

[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 Ω\Omega 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 Ω\Omega

view this post on Zulip Matteo Capucci (he/him) (Oct 14 2020 at 14:16):

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

view this post on Zulip Jacques Carette (Oct 14 2020 at 14:20):

Equivalence predicate. Without J, I don't tend to call an equivalence relation an 'equality'.

view this post on Zulip Matteo Capucci (he/him) (Oct 14 2020 at 14:22):

J?

view this post on Zulip Jacques Carette (Oct 14 2020 at 14:24):

The computational J rule for identity elimination for identity types in Martin-Loef Type Theory. It's derivable from Yoneda, as per Martin Escardo.

view this post on Zulip Matteo Capucci (he/him) (Oct 14 2020 at 14:28):

Uh wow, I didn't know any of that

view this post on Zulip sarahzrf (Oct 14 2020 at 14:41):

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

view this post on Zulip sarahzrf (Oct 14 2020 at 14:49):

more broadly:

view this post on Zulip sarahzrf (Oct 14 2020 at 14:51):

...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"

view this post on Zulip James Wood (Oct 14 2020 at 14:57):

Matteo Capucci said:

Uh wow, I didn't know any of that

Type theorists, equality, &c. :laughter_tears:

view this post on Zulip Reid Barton (Oct 14 2020 at 15:01):

Matteo Capucci said:

J?

Speaking of bad names...

view this post on Zulip Dan Doel (Oct 14 2020 at 16:23):

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.

view this post on Zulip Dan Doel (Oct 14 2020 at 16:23):

Leibniz' characterization or something.

view this post on Zulip Jacques Carette (Oct 14 2020 at 17:18):

@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.

view this post on Zulip sarahzrf (Oct 14 2020 at 17:35):

i should take a look at agda-categories one of these days :thinking: