Zulip Chat Archive

Stream: general

Topic: programming


view this post on Zulip 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

view this post on Zulip Simon Hudon (Jun 29 2020 at 12:40):

Maybe programming would be a more unambiguous name

view this post on Zulip Gabriel Ebner (Jun 29 2020 at 12:46):

How about burrito?

view this post on Zulip 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.

view this post on Zulip Simon Hudon (Jun 29 2020 at 12:49):

I heard monads aren't burrito @Gabriel Ebner, it might be slightly inaccurate

view this post on Zulip Johan Commelin (Jun 29 2020 at 12:50):

@Simon Hudon That was fake news. Scientists have established that monads are, in fact, burrito.

view this post on Zulip Johan Commelin (Jun 29 2020 at 12:50):

The converse fails... some burritos aren't monadic.

view this post on Zulip 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!

view this post on Zulip Mario Carneiro (Jun 29 2020 at 13:46):

are burritos compositional?

view this post on Zulip Anne Baanen (Jun 29 2020 at 13:48):

Looks like it's time for Burritos for the Hungry Mathematician again!

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jun 29 2020 at 14:00):

Maybe Kevin should wrap his division and nat subtraction in a burrito instead...

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Simon Hudon (Jun 29 2020 at 16:13):

Did it lose any nice mathematical properties?

view this post on Zulip Johan Commelin (Jun 29 2020 at 16:30):

No... it just lived in a higher universe

view this post on Zulip Simon Hudon (Jun 29 2020 at 16:39):

But didn't you say you saw that in the states?

view this post on Zulip Johan Commelin (Jun 29 2020 at 16:43):

It had "Russell" written all over it.


Last updated: May 11 2021 at 21:10 UTC