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: enriched category

Leopold Schlicht (Mar 04 2022 at 18:22):

Is there a sensible notion of $C$-enriched category (for $C$ a concrete category) considered in the literature in which not only the "hom-sets" are objects of $C$ but also the "collection of objects"? That idea is related to the notion of a category internal to $C$ - however, I'd like to work with dependent-type "hom-sets" rather than one large "collection" of all morphisms. In particular I'm interested in $C=\mathbf{Top}$. Then functors between such $C$-enriched categories should be required to be continuous on objects in addition to being continuous on the "hom-sets", for instance.

Mike Shulman (Mar 04 2022 at 18:27):

Whether you think of the hom-sets as dependent types or as a single collection is orthogonal to the question of internalization. It's true that the usual definition of internal category is phrased using the single-collection approach, but if you write the dependent-type version in the internal dependent type theory of a finite-limit category you end up with the same external notion.

Mike Shulman (Mar 04 2022 at 18:28):

That said, depending on your goal you might be interested in my paper Enriched indexed categories which studies categories whose collection of objects is internal to one category and whose collections of morphisms are enriched in a different category (which is fibered over the first).

Leopold Schlicht (Mar 04 2022 at 18:43):

Mike Shulman said:

It's true that the usual definition of internal category is phrased using the single-collection approach, but if you write the dependent-type version in the internal dependent type theory of a finite-limit category you end up with the same external notion.

That's amazing, thanks!

Suppose I specify a category internal to Top using the dependent-type version, i.e., I give a family of local hom-spaces. How do I obtain the corresponding global space of all morphisms?

Mike Shulman (Mar 04 2022 at 18:45):

Internally, it would be $\sum_{x,y:{\rm ob}(C)} \hom(x,y)$. Externally, the dependent type $x:{\rm ob}(C), y:{\rm ob}(C) \vdash \hom(x,y) : \rm type$ is interpreted by a display map ${\rm arr}(C) \to {\rm ob}(C) \times {\rm ob}(C)$, so it is already the total space.

Leopold Schlicht (Mar 04 2022 at 18:53):

Mhm, I see, but I mean: if I, while working externally, specify a space $X\in \mathbf{Top}$ (with underlying set $U(X)$) and for all $x,y\in U(X)$ a space $\hom(x,y)\in\mathbf{Top}$, is there a canonical way to compile that into a topological category?

Also, is there literature about the internal dependent type theory of a finite-limit category?

Mike Shulman (Mar 04 2022 at 18:59):

is there a canonical way to compile that into a topological category?

No, that's not possible in general: an internal category in Top is more than just a Top-enriched category with an unrelated topology on the set of objects.

Mike Shulman (Mar 04 2022 at 19:03):

is there literature about the internal dependent type theory of a finite-limit category?

Not as much as there is about that for locally cartesian closed categories, but there's some. There's a nice long systematic treatment of dependent type theories for categories with different fragments of logic, but I can't remember at the moment by who or what it's called...

Leopold Schlicht (Mar 05 2022 at 12:57):

is there a canonical way to compile that into a topological category?

No, that's not possible in general: an internal category in Top is more than just a Top-enriched category with an unrelated topology on the set of objects.

Thanks! Is "Top-enriched category with an unrelated topology on the set of objects" nevertheless a sensible notion to consider?

Mike Shulman (Mar 05 2022 at 17:08):

Not really. In general, whenever you have multiple structures you should ask them to cohere.

Fawzi Hreiki (Mar 05 2022 at 18:00):

I guess you’d at least want the core of the category to be the fundamental groupoid of the space of objects

Mike Shulman (Mar 05 2022 at 18:17):

No, here we're talking about topologies up to point-set isomorphism, not homotopy equivalence.

Leopold Schlicht (Mar 06 2022 at 12:38):

Thanks!