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?

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?

Matteo Capucci (he/him) (Oct 14 2020 at 11:30):

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

Matteo Capucci (he/him) (Oct 14 2020 at 11:31):

Terminologically though, I don't now

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.

Matteo Capucci (he/him) (Oct 14 2020 at 11:36):

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

James Wood (Oct 14 2020 at 12:12):

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

Jacques Carette (Oct 14 2020 at 12:17):

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

Fabrizio Genovese (Oct 14 2020 at 12:44):

Matteo Capucci said:

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

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.

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?

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:

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.

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

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.

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.

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?

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.

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.

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

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$

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

Jacques Carette (Oct 14 2020 at 14:20):

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

Matteo Capucci (he/him) (Oct 14 2020 at 14:22):

J?

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.

Matteo Capucci (he/him) (Oct 14 2020 at 14:28):

Uh wow, I didn't know any of that

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

sarahzrf (Oct 14 2020 at 14:49):

more broadly:

• an object whose yoneda embedding is a functor valued in that subcategory of Set is gonna be precisely a subterminal object
• given some Set-flavored category, it's of interest to ask whether the full subcategory of subterminals—which is always a preorder—is reflective, as it is in Set, because that will be a kind of "propositional truncation"
• given a category with finite limits, it's further of interest to ask whether it locally admits that, in the sense of "slices have the thing and pullback respects it"—i.e., whether we have reflective subterminals in each slice category, and the base change functors commute with the reflections. that's exactly a regular category

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"

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:

Reid Barton (Oct 14 2020 at 15:01):

Matteo Capucci said:

J?

Speaking of bad names...

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.

Dan Doel (Oct 14 2020 at 16:23):

Leibniz' characterization or something.

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.

sarahzrf (Oct 14 2020 at 17:35):

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