Zulip Chat Archive
Stream: general
Topic: programming
Simon Hudon (Jun 29 2020 at 12:40):
That reminds me. We might want to rename the control directory again: in case people come in with some control theory. Although, maybe that should go in a different library
Simon Hudon (Jun 29 2020 at 12:40):
Maybe programming would be a more unambiguous name
Gabriel Ebner (Jun 29 2020 at 12:46):
How about burrito?
Patrick Massot (Jun 29 2020 at 12:47):
The advantage is it would clearly tell people who don't get the reference that this folder is not for them.
Simon Hudon (Jun 29 2020 at 12:49):
I heard monads aren't burrito @Gabriel Ebner, it might be slightly inaccurate
Johan Commelin (Jun 29 2020 at 12:50):
@Simon Hudon That was fake news. Scientists have established that monads are, in fact, burrito.
Johan Commelin (Jun 29 2020 at 12:50):
The converse fails... some burritos aren't monadic.
Simon Hudon (Jun 29 2020 at 12:52):
Is that because burritos are merely semigroups in the category of endofunctors? I think that's reassuring. I wouldn't want to eat an identity burrito, oh no!
Mario Carneiro (Jun 29 2020 at 13:46):
are burritos compositional?
Anne Baanen (Jun 29 2020 at 13:48):
Looks like it's time for Burritos for the Hungry Mathematician again!
Simon Hudon (Jun 29 2020 at 13:56):
Mario Carneiro said:
are burritos compositional?
I haven't proved the laws but when I see two burritos on the table, I unwrap them, put them end-to-end and rewrap them as one. It seems associative to me
Reid Barton (Jun 29 2020 at 13:57):
But if they're different kinds of burritos, then all the ingredients spill out everywhere and it makes a big mess.
Simon Hudon (Jun 29 2020 at 13:59):
It is true but as long as you get the same result of you combine the chicken and beans first and then the beef and when you start with beans and beef and then you put it with the chicken, I think you can call it a day
Johan Commelin (Jun 29 2020 at 14:00):
Maybe Kevin should wrap his division and nat subtraction in a burrito instead...
Bhavik Mehta (Jun 29 2020 at 16:08):
"we have assumed all burritos to be at least locally small" I'm so disappointed I hadn't read this paper sooner
Johan Commelin (Jun 29 2020 at 16:09):
I think when I visited the USA, at some point I saw a large burrito. It was quite shocking.
Simon Hudon (Jun 29 2020 at 16:13):
Did it lose any nice mathematical properties?
Johan Commelin (Jun 29 2020 at 16:30):
No... it just lived in a higher universe
Simon Hudon (Jun 29 2020 at 16:39):
But didn't you say you saw that in the states?
Johan Commelin (Jun 29 2020 at 16:43):
It had "Russell" written all over it.
Last updated: Dec 20 2023 at 11:08 UTC