Stream: Is there code for X?

Topic: Continuous algebra homomorphisms

Scott Morrison (Mar 17 2021 at 10:47):

Ugh, I want to talk about continuous algebra homomorphisms.

I can't bear the thought of building yet another bundled structure, with pages of API about equivalences and subobjects and so on.

Scott Morrison (Mar 17 2021 at 10:48):

Can I just define the category TopAlgebra and work there? :-)

Johan Commelin (Mar 17 2021 at 10:52):

who knows... if it works, that would be great.

Johan Commelin (Mar 17 2021 at 10:52):

We really need the structure bundle builder gadget that people talked about at LT2021

Eric Wieser (Mar 17 2021 at 11:17):

Scott Morrison said:

Can I just define the category TopAlgebra and work there? :-)

Scott, is it remotely viable to use this approach everywhere, and build the non-category API as a thin later on top of the category API?

Scott Morrison (Mar 18 2021 at 12:29):

The thing you immediately lose is the ability to talk about homomorphisms between objects at different universe levels.

Scott Morrison (Mar 18 2021 at 12:30):

This is pretty annoying.

Eric Wieser (Mar 18 2021 at 13:00):

Are there situations where that makes statements weaker, or is it just super annoying but not strictly limiting (in that you need ulift everywhere)?

Kevin Buzzard (Mar 18 2021 at 13:03):

Scott says "this is pretty annoying" wrt this universe polymorphic stuff, however I spent 25 years of my life doing research mathematics without the ability to talk about homomorphisms between objects at different universe levels and this didn't bother me in the slightest.

Kevin Buzzard (Mar 18 2021 at 13:05):

Sticking to homs between objects of the same type is far less of an extreme restriction than my usual "why not just let everything be Type or Prop" rant which usually comes out at this point. This lets people be universe-polymorphic but not multi-polymorphic. Do we really need maps between groups of type u and type v in any application, or do we just do them because we can?

Eric Wieser (Mar 18 2021 at 13:08):

There's no way to generalize over both Type and Prop without also generalizing over all universes though, right?

Scott Morrison (Mar 18 2021 at 13:26):

@Eric Wieser, yes, but that's still orthogonal to Kevin's point.

Scott Morrison (Mar 18 2021 at 13:27):

I agree, I think, Kevin. Perhaps what I meant is that "it is pretty annoying that people bring this up as an objection". :-)

Johan Commelin (Mar 18 2021 at 13:29):

@Kevin Buzzard you've also spent 25 years of your life believing that $R[1/fg] = R[1/f][1/g]$...

Eric Wieser (Mar 18 2021 at 13:29):

Ah, I misread "type or prop" as "some wildcard that covers both" not "just pick one each time"

Kevin Buzzard (Mar 18 2021 at 13:32):

Yes I agree that it's annoying that there's no wildcard which covers both, however mathematicians are very good at distinguishing between them (for example I was carefully taught that the recursor from nat to Type was called "construction by recursion" and the recursor to Prop was called "proof by induction"). In my teaching tools there are Type and Prop everywhere and it's very rare that I want to explicitly unify these things. Mathematicians even have an arrow $\to$ for Type and a different arrow $\implies$ for Prop.

Eric Wieser (Mar 18 2021 at 13:38):

Perhaps a good example of where unifying the two is useful is docs#set.Union, which enables the bounded union notation; but I agree even those cases are rare

Yury G. Kudryashov (Mar 18 2021 at 20:55):

Usually at this point of discussion @Mario Carneiro comes to the room and tells us about some exotic cases in parts of math I don't understand where it's important to have different universes. I still wonder if it's easier to use category theory almost everywhere and use ulift whenever we really need different universes.

Yury G. Kudryashov (Mar 18 2021 at 20:56):

One downside of using category theory homs everywhere is that we loose tricks like "monoid_hom both for monoid and group homs"

Mario Carneiro (Mar 18 2021 at 20:56):

I'm sympathetic to this point of view, but it doesn't really work to have everything in Type u (i.e. polymorphic but with only one universe) because lots of things are in Type

Mario Carneiro (Mar 18 2021 at 20:57):

I mean you can get by with ulift but it's really inconvenient

Yury G. Kudryashov (Mar 18 2021 at 20:57):

Indeed, we can't stick to "everything in Type u" without nat.{u} and real.{u}.

Good point.

Yury G. Kudryashov (Mar 18 2021 at 20:58):

(and we probably don't want to have lots of different nats around.

Mario Carneiro (Mar 18 2021 at 20:58):

The theory of cardinals does essentially this

Mario Carneiro (Mar 18 2021 at 20:58):

omega.{u} is defined as mk (ulift nat)

Mario Carneiro (Mar 18 2021 at 20:59):

It's also annoying to have universe parameters that aren't inferred because you usually can't omit them, i.e. you will actually be writing nat.{u} most of the time

Mario Carneiro (Mar 18 2021 at 21:02):

I recall early in the category theory development I suggested pinning the second universe argument of category (for the homs) to either v=u or v=u+1, but Scott argued that we want to prove things generic over both, so now we have two universe params. And once you start doing that it's really unnatural to restrict the parametricity in some specific areas because you wind up revising it eventually anyway (like the recent example with limit`)

Last updated: May 16 2021 at 05:21 UTC