# Zulip Chat Archive

## Stream: maths

### Topic: With Category Theory, Mathematics Escapes From Equality

#### Olli (Oct 10 2019 at 18:07):

what do the mathematicians here think about this article: With Category Theory, Mathematics Escapes From Equality ?

#### Olli (Oct 10 2019 at 18:13):

something I found interesting having just watched *The Future of Mathematics* talk was finding out that topos theory is such a big deal amongst mathematicians, having only had exposure to it from studying type theory

#### Olli (Oct 10 2019 at 18:15):

in his talk @Kevin Buzzard said that the category theorists are retiring, but I would have considered topos theory to be a subfield of category theory

#### Johan Commelin (Oct 10 2019 at 18:24):

@Olli It's a well-written overview of a revolution that has been ripping through parts of mathematics in the last few years.

#### Johan Commelin (Oct 10 2019 at 18:25):

It's quite clear by now that infty-cats will play a big role in future maths. Most people are sort of warming up to them. But personally, I haven't seriously used them yet.

#### Johan Commelin (Oct 10 2019 at 18:25):

(Also, thanks for the link.)

#### Johan Commelin (Oct 10 2019 at 18:27):

One thing that I would really like to see is a good connection between HoTT and Lurie's infty-cats. Maybe @Reid Barton knows if there is a good article on this?

#### Olli (Oct 10 2019 at 18:27):

if formalization of FLT costs $100M, how much would it cost to formalize Lurie's work? it would this work be significantly different from the type of work that goes into proving FLT?

#### Johan Commelin (Oct 10 2019 at 18:28):

Yes, I think formalizing Lurie is easier. Possibly even easier when done in HoTT.

#### Johan Commelin (Oct 10 2019 at 18:29):

The amount of pages is a lot less, and the literature is quite linearly structured.

#### Johan Commelin (Oct 10 2019 at 18:29):

But then, I'm really an amateur on both these things.

#### Olli (Oct 10 2019 at 18:30):

would saying that formalising this type of work is more breadth oriented vs. depth oriented compared to proof of FLT be correct?

#### Johan Commelin (Oct 10 2019 at 18:31):

In some sense, yes, I think

#### Olli (Oct 10 2019 at 18:32):

so is there a chance that if you started with infinity categories, you'd actually finish the proof of FLT faster, because you had more flexible tools, or would that be something completely different?

#### Olli (Oct 10 2019 at 18:32):

the book I have on topos theory that I only just began reading presents it as a foundational system

#### Olli (Oct 10 2019 at 18:33):

and my impression is that most mathematicians care very little about foundational issues

#### Olli (Oct 10 2019 at 18:34):

but maybe they would care if it made their work easier? is that the promise?

#### Johan Commelin (Oct 10 2019 at 18:35):

Yes. But I think it wouldn't help very much for FLT

#### Johan Commelin (Oct 10 2019 at 18:36):

Although it would probably help if one were to really formalise parts of étale cohomology.

#### Olli (Oct 10 2019 at 18:36):

yeah I'm now really curious about the relationship between topos theory and HoTT, would love to hear more about that

#### Johan Commelin (Oct 10 2019 at 18:36):

And everything involving derived categories.

#### Johan Commelin (Oct 10 2019 at 18:37):

So yes, some parts of the FLT proof would be affected. But I wouldn't expect a major speed up. You'll lose more time by first formalising all Luries stuff, I guess.

#### Johan Commelin (Oct 10 2019 at 18:37):

Note, it's not just topos theory. It's *higher* topos theory.

#### Johan Commelin (Oct 10 2019 at 18:37):

Topos theory has been around for ages (-;

#### Johan Commelin (Oct 10 2019 at 18:39):

But for example, in the recent lecture notes by Scholze on condensed mathematics, he needs to glue some derived categories... this doesn't actually work. So what he does instead is climb up this infty-tower, and glue some infty-categories instead. That's a thing where these infty-categories really pay off.

#### Olli (Oct 10 2019 at 18:44):

that's cool, I wonder if there are any practical applications of infinity-CT outside of mathematics, besides perhaps in theorem proving (via HoTT)?

#### Reid Barton (Oct 10 2019 at 21:53):

The amount of pages is a lot less, and the literature is quite linearly structured.

In fact Jacob's current project https://kerodon.net/ is almost entirely self-contained.

On the other hand it hasn't quite gotten to the point where Higher Topos Theory begins yet

#### Ulrik Buchholtz (Oct 11 2019 at 07:38):

Re the connection between HoTT and (∞,1)-categories in set theoretic foundations: This is unfortunately a very sore spot for HoTT at the moment, as we don't know how to define the *type* of (∞,1)-categories. (We could do if we knew how to define the type of semi-simplicial types, but we don't.) Of course, we *can* define quasi-categories, but we then need to take the ∞-groupoid quotient by the Joyal equivalences, and we don't know how to do that. These problems all seem to require each other for their solution in HoTT, and noone knows where to start.

Note that this problem with analytically defining (∞,1)-categories etc. in HoTT occurs because we aim to represent higher mathematical objects by their correct type/∞-groupoid, and we're not content with a set-presentation thereof.

There is a work-around: work in HoTT as modeled in simplicial ∞-groupoids/spaces. Then we can work with (∞,1)-categories synthetically as complete Segal types, cf. Riehl-Shulman.

I wrote a book chapter for philosophers discussing these issues: Higher Structures in Homotopy Type Theory, and the situation is basically unchanged. (Meanwhile, there were a couple of promising attempts, but so far no luck.)

#### Kevin Buzzard (Oct 11 2019 at 07:42):

Thanks for this, Ulrik! Something that perhaps should be stressed on this thread is that Lurie's work is not just navel-gazing -- his work on these higher categories actually has applications in what I have sarcastically referred to in the past as "proper mathematics" (although this strategy is beginning to get me into trouble so perhaps I should stop doing it). So ultimately these questions will need to be solved.

#### Ulrik Buchholtz (Oct 11 2019 at 07:48):

Oh yes, and even applications to mathematical physics/foundations of physics, cf. e.g. work by Urs Schreiber and collaborators.

#### Patrick Massot (Oct 11 2019 at 08:16):

It's a well-written overview of a revolution that has been ripping through parts of mathematics in the last few years.

It's quite clear by now that infty-cats will play a big role in future maths. Most people are sort of warming up to them. But personally, I haven't seriously used them yet.

Notice for casual readers: 99.9% of mathematicians don't even know that infinity-categories exist and, most likely, they will never care. But people who love that stuff have a very strong tendency to oversell it, most probably because it's a very heavy technology that takes longer than expected to deliver applications (to abstract mathematics, not to the real world). Personally I'd love to know more about this stuff, but I really think that kind of propaganda should not exist in mathematics.

#### Johan Commelin (Oct 11 2019 at 08:18):

You are right... I should have better delimited this to e.g. arithmetic geometry and algebraic topology/homotopy theory.

#### Keeley Hoek (Oct 11 2019 at 08:21):

We had an undergraduate (infinity,1)-categories (as quasicategories) course last year!

#### Kevin Buzzard (Oct 11 2019 at 09:46):

Are you talking about ANU maths department?

#### Keeley Hoek (Oct 11 2019 at 10:02):

That's right.

#### Scott Morrison (Oct 11 2019 at 10:08):

(For the record, this had nothing to do with me. :-)

#### Scott Morrison (Oct 11 2019 at 10:09):

(And so now all the undergrads know more about (\infty,1)-categories than I do.)

#### Johan Commelin (Oct 11 2019 at 11:21):

You should make them formalise it :rolling_on_the_floor_laughing:

#### Patrick Massot (Oct 11 2019 at 11:24):

I just read the Quanta article. Unsurprisingly it loves the genius story, but I'm pretty sure many people will be very upset by how little they say about previous work.

#### David Michael Roberts (Oct 12 2019 at 07:23):

One thing that I would really like to see is a good connection between HoTT and Lurie's infty-cats.

(not really Lurie's infinity-cats, but I know what you mean)

Work of Mike Shulman is relevant here: https://arxiv.org/abs/1904.07004, the abstract reads in part

We prove the conjecture that any Grothendieck (∞,1)-topos can be presented by a Quillen model category that interprets homotopy type theory with strict univalent universes. Thus, homotopy type theory can be used as a formal language for reasoning internally to (∞,1)-toposes, just as higher-order logic is used for 1-toposes.

Last updated: May 11 2021 at 00:31 UTC