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: theory: philosophy

Topic: univalence irl

Henry Story (Sep 12 2020 at 13:52):

Jules Hedges said:

... the questions channel could quickly degenerate into MathOverflow levels of unfriendly

This reminds me of a fun question I asked on Math Overflow nearly 3 years ago regarding HoTT, which they promptly closed, even though it got a lot of interesting and fun answers, there and on the HoTT café mailing list.

This was the question:

If my wife gives me a set of things to buy, eg. A = { sugar, flour, eggs, milk } and I come back with B = { wine, whiskey, cigars, newspaper } then both sets are isomorphic, but my wife won't be happy.

Why can't I invoke the Univalence Axiom in my defense to show that isomorphic things are identical?

Jules Hedges (Sep 12 2020 at 13:57):

Heh, nice question

Jules Hedges (Sep 12 2020 at 13:58):

I'd say that it's a great philosophical logic question but not a mathematics question, which probably explains why it was closed

Henry Story (Sep 12 2020 at 14:00):

I wonder how one draws that boundary? (But I guess that is a philosophical logic question) ;-)

Matteo Capucci (he/him) (Sep 12 2020 at 14:31):

Very cool question indeed. Checkmate, mathematics :)

Jules Hedges (Sep 12 2020 at 14:42):

My answer would be, in such a microeconomic situation the basic objects are not sets but preference relations, and your bijection is not an isomorphic on the level of preference relations

Henry Story (Sep 12 2020 at 15:02):

That's a great answer. It brings out how objects live in subjective spaces.

Jules Hedges said:

I'd say that it's a great philosophical logic question but not a mathematics question, which probably explains why it was closed

In answer to that I should point to @Mike Shulman answer in the comments at the time:

Yes, this is at least isomorphic to a mathematical question; hence, by univalence, it is itself a mathematical question!

Reid Barton (Sep 12 2020 at 15:04):

So the real question is why can't you use the univalence axiom to argue that the question is suitable for MO

Mike Shulman (Sep 12 2020 at 15:07):

Probably because the MO moderators don't believe in univalence yet. (-:

Mike Shulman (Sep 12 2020 at 15:09):

BTW, the link @Henry Story gave above goes to an (invisible) question on MSE, not MO.

Henry Story (Sep 12 2020 at 15:21):

Ah yes, quite right, it was Math Stack Exchange. I just posted a screen shot of the answers given there for reference. In the end I posted a (near) isomorphic question in a more mathematical style only mentioning numbers which also got good answers. But I think @Jules Hedges answer above gets an important aspect that is lost if one only looks at numbers.

Many good answers to a closed question on Math Stack Exchange regarding the HoTT univalence axiom and shopping. https://twitter.com/bblfish/status/1304801157794222081/photo/1

- The 🐟‍‍ BabelFish (@bblfish)

Nikolaj Kuntner (Sep 13 2020 at 01:19):

If my wife gives me a set of things to buy, eg.
A = { sugar, flour, eggs, milk } and I come back with
B = { wine, whiskey, cigars, newspaper } then both sets are isomorphic,
but my wife won't be happy.

I'd say the language for this is discussed in Das Kapital, where Marx defines use-value, exchange-value, and all that.
He actually wrote math papers, but I can't speak for their value :)
Maybe he'd be a HoTT guy if he lived today.

Nikolaj Kuntner (Sep 13 2020 at 01:26):

Bildschirmfoto-2020-09-13-um-03.26.27.png
:working_on_it:

Henry Story (Sep 13 2020 at 08:40):

I think one good answer is that my wife will tell me she asked me to get an instance of the type
$\text{Sugar} \times \text{Flour} \times \text{Eggs} \times \text{Milk}$
ie
$(s,f,e,m): \text{Sugar} \times \text{Flour} \times \text{Eggs} \times \text{Milk}$
and that is isomorphic to each combinations of those types eg:
$(m,e,f,s): \text{Milk} \times \text{Eggs} \times \text{Flour} \times \text{Sugar}$
even to
$(m,e,f,s,*): \text{Milk} \times \text{Eggs} \times \text{Flour} \times \text{Sugar} \times \mathbf{1}$
But none of those types are isomorphic to
$(w,w',c,n): \text{Wine} \times \text{Whiskey} \times \text{Cigars} \times \text{Newpaper}$

Morgan Rogers (he/him) (Sep 13 2020 at 10:25):

Aha! The things on your shopping list were not just elements of a set, but objects of a category, and the objects you brought back failed to have the required universal properties... :thinking: You didn't bring home the initial objects from the subcategories of dairy products and baked goods, for example, although the colimit of all communicated events up to this morning was a reasonable purchase choice.

Nikolaj Kuntner (Sep 13 2020 at 16:09):

Why yes, my girlfriend wouldn't send me to bring home { sugar, flour, eggs, milk }, he's ask for buying { hom(-, sugar), hom(-, flour), hom(-, eggs), hom(-, milk) }

Henry Story (Sep 13 2020 at 19:57):

I was pointed to this fun article Burritos for the Hungry Mathematician.
The Abstract:

The advent of fast-casual Mexican-style dining establishments, such as Chipotle and Qdoba, has greatly improved the productivity of research mathematicians and theoretical computer scientists in recent years. Still, many experience confusion upon encountering burritos for the first time. Numerous burrito tutorials (of varying quality) are to be found on the Internet. Some describe a burrito as the image of a crêpe under theaction of the new-world functor. But such characterizations merely serveto reindex the confusion contravariantly. Others insist that the only wayto really understand burritos is to eat many different kinds of burrito, until the common underlying concept becomes apparent. It has been recently remarked by Yorgey [9] that a burrito can be regarded as an instance of a universally-understood concept, namely, that of a monad. It is this characterization that we intend to explicate here. To wit, a burrito is just a strong monad in the symmetric monoidal category of food, what’s the problem?

Notification Bot (Sep 14 2020 at 21:08):

This topic was moved here from #general > Community by Matteo Capucci

David Michael Roberts (Sep 16 2020 at 05:21):

Compare this to asking why sets {x,y,z} and {a,b,c} should/could be considered equal in HoTT. They are isomorphic. Are they equal (as sets, not as subsets of the set of latin letters)?

Henry Story (Sep 16 2020 at 06:48):

Andreij Bauer's answer is probably the best as it does not get lost in questions of the types but starts with what it would be to accept the equivalence. He wrote:

Suppose $e : \{1, 2,3\} \to \{4, 5, 6\}$ is an equivalence. By Univalence axiom there is a path $\mathsf{ua}(e) : \{1, 2,3\} = \{4, 5, 6\}$. There is a path
$p : \sup \{1, 2, 3\} = 3.$
In order to apply univalence to $\{1, 2, 3\}$ in this situation, we have to transport $\{1, 2, 3\}$ as well as $\sup$, $p$ and the element $3$ along the path $\mathsf{ua}(e)$. What we get is something like
$\mathsf{ua}(e) \cdot p : (e \circ \mathsf{sup} \circ e^{-1}) \{4, 5, 6\} = e(3).$
I am not trying to be precise here, because we are already quite sloppy by writing set-theoretic stuff like $\{1, 2, 3\}$ and $\{4, 5, 6\}$, but I hope you get the idea: You have to explicitly transport the entire statement along the equivalence.

I think those are actually great examples to motivate one to think about that transportation function. The necessary maths is covered in chapter 1.12 and 2 of The HoTT Book which is very readable btw.

Fawzi Hreiki (Sep 26 2020 at 18:38):

Well the reason you can't invoke univalence is that your wife does not just see A and B as pure abstract sets - otherwise she would not have asked for sugar, flour, eggs, and milk, but instead for any four 'things'. In this context, the type A signifies something more like a 'space of ingredients for making a cake' which is something the type B is 'far away from'.