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: Homotopified double categories

David Corfield (May 20 2024 at 09:17):

If the wish to represent both the functional and relational aspects of mathematics in double categories has motivations from logic, is there importance for logic in the concept of double $\infty$-categories, as devised by Lurie and Haugseng (cf. here)? Is there any value in a form of HoTT treating spans separately?

Kevin Carlson (May 21 2024 at 02:33):

I certainly think that any of the advantages of double categories over bicategories would be realized, probably all the moreso, with double $\infty$-categories. The "logic" of categories is really a logic of functors and profunctors, and this is true of $\infty$-categories too. But I don't think this is quite the same thing as getting a different form of HoTT, since HoTT is modeled by $\infty$-groupoids, not $\infty$-categories. Riehl and Shulman have some work on "directed HoTT", where every type is structured as an $\infty$-category, and it would seem to be a more relevant question there whether we should want the profunctors explicitly in the syntax. New and Cicala have a paper defining a type theory called VETT with semantics in virtual equipments, but without anything $\infty$ about it; I guess it's something like this one would have to try to generalize. But Riehl and Verity's book shows, to my mind, that an awful lot of the logical content of $\infty$-category theory lies in the ordinary (virtual) equipment of $\infty$-categories. I kind of think you might not really want the full double $\infty$ structure all at once in your type theory, rather than some kind of ordinary HoTT for the $\infty$-groupoid hom-spaces and some kind of VETT-like thing for the non-groupoidal part of the story.

Mike Shulman (May 21 2024 at 03:42):

The problem with the ordinary equipment of $\infty$-categories is that its 2-cells are quotiented. That's good enough for a lot, but when it's not good enough, you're kind of stuck because you can't get "out" of the quotient. Working in HoTT we often get many of the benefits of quotienting because we can just talk about however much coherence we need and ignore the rest; so my inclination would be that a VETT that's "homotopical on the proarrows" would be the nicest place to work.

David Corfield (May 21 2024 at 06:19):

Kevin Carlson said:

New and Cicala have a paper defining a type theory called VETT with semantics in virtual equipments

Presumably that's New and Licata in A Formal Logic for Formal Category Theory.

John Baez (May 21 2024 at 06:27):

Darn, I was hoping my student Daniel Cicala had re-emerged as an infinity-category theorist!

Kevin Carlson (May 21 2024 at 06:34):

Hm, it’s a lot of the same letters…

David Corfield (May 21 2024 at 09:45):

Thanks, Kevin and Mike.

And if I may be allowed one more piece of speculative wondering, do people see any place for whatever a 'double topos' (sec 12.3 of Lambert's Double Categories of Relations may turn out to be, and from there a 'double $\infty$-topos?

John Baez (May 21 2024 at 09:51):

To escalate the speculation to an absurd degree: when trying to understand the best concept of $\infty$-equipment, is there a natural reason to go beyond double $\infty$-categories to triple $\infty$-categories, quadruple $\infty$-categories, and so on ad infinitum?

John Baez (May 21 2024 at 09:56):

Here's maybe a better way to put my question. In Cat or Gpd it turns out to be useful to think about profunctors as well as functors, and these two kinds of arrow organize themselves nicely into a double category. When we go to 2Cat or $(2,1)$-Cat, is there something that really seems naturally to continue the sequence

functors, profunctors, .... ?

John Baez (May 21 2024 at 09:57):

@Christian Williams may say "of course", but I don't understand the general pattern.

David Corfield (May 21 2024 at 13:28):

Back in the 'real' world of mathematics, from that Haugseng article I mentioned above:

if $\mathbf{V}$ is a reasonable $E_n$-monoidal $\infty$-category, then there is an $(n + 1)$-fold $\infty$-category of $E_n$-algebras and iterated bimodules in $\mathbf{V}$.

Christian Williams (May 21 2024 at 17:29):

John Baez said:

Christian Williams may say "of course", but I don't understand the general pattern.

A double category has two kinds of morphisms, so DblCat has functors and two kinds of profunctors.

TrpCat has functors and three kinds of profunctors, etc... that's the pattern.

Mike Shulman (May 21 2024 at 18:32):

David Corfield said:

And if I may be allowed one more piece of speculative wondering, do people see any place for whatever a 'double topos' (sec 12.3 of Lambert's Double Categories of Relations) may turn out to be, and from there a 'double $\infty$-topos?

I don't know; I kind of feel a lack of examples. E.g. are there double toposes other than those obtained from internal profunctors in some 2-topos?

David Kern (May 22 2024 at 16:47):

David Corfield said:

Back in the 'real' world of mathematics, from that Haugseng article I mentioned above:

if $\mathbf{V}$ is a reasonable $E_n$-monoidal $\infty$-category, then there is an $(n + 1)$-fold $\infty$-category of $E_n$-algebras and iterated bimodules in $\mathbf{V}$.

That is true; however this $(n+1)$-uple $\infty$-category is symmetric in all but the "$+1$" directions (in much the same way as the $(n+1)$-uple categories of $n$-iterated spans).