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: learning: reading & references

Topic: A Rosetta Stone

Jake Gillberg (Apr 18 2020 at 20:02):

A couple of friends (of mostly programming and some maths background) are planning to read "Physics, Topology, Logic and Computation:A Rosetta Stone" and do some poking in Idris to guide our understanding. We plan to look over these overview slides / notes (http://math.ucr.edu/~mike/rosettaslides.pdf), (http://math.ucr.edu/~mike/rosetta%20slides.txt), read through section 2.4 of the paper, and meet next Saturday at 1:00 (GMT -4) to discuss

Jake Gillberg (Apr 18 2020 at 20:04):

please chime in if you are interested in joining!

T Murrills (Apr 18 2020 at 20:08):

Looks interesting! Count me in! :)

John Baez (Apr 18 2020 at 22:09):

Great! I'd be happy to answer any questions here.

Naso (Apr 20 2020 at 12:59):

I'm also keen. Is that 1:00 AM or PM GMT-4? I'm GMT+10.

Luc Chabassier (Apr 20 2020 at 16:43):

Sounds interesting, I'd gladly join ! As Nasos I am a bit confused about the meeting time, could you give the UTC meeting time ? Thanks !

Christian Williams (Apr 20 2020 at 17:36):

Great! I'm sure @Mike Stay would be happy to talk about it here as well.

Reid Barton (Apr 20 2020 at 17:39):

I would assume that someone giving a time in GMT -4 lives in that time zone and is not scheduling an event for 1 AM local time.

Jake Gillberg (Apr 20 2020 at 18:49):

Great! Yes, I meant 1PM (GMT -4) or 17 UTC. We can try to shuffle the time around to make it better for all who want to attend. Here is a survey to see when folks may be available: https://xoyondo.com/dp/9goetOGA6VSwF7q . In the upper left corner, you can change the times to your timezone.

Mike Stay (Apr 20 2020 at 21:34):

Christian Williams said:

Great! I'm sure Mike Stay would be happy to talk about it here as well.

Yep!

Jake Gillberg (Apr 23 2020 at 23:32):

Looks like the original time of 17UTC this Saturday remains the crowd favorite. Hope to see you all there!

Reminder that the goal is to look over these slides & corresponding notes, and read up to section 2.5: Symmetric Monoidal Categories in the paper prior to our meeting.

T Murrills (Apr 25 2020 at 15:04):

(Today’s my SO’s birthday, so I’m afraid I won’t be there today, but I’ll definitely be there next time! :) )

sarahzrf (Apr 25 2020 at 15:15):

seems kinda weird to celebrate your stackoverflow account's birthday but programmers will be programmers i guess

Cody Roux (Apr 25 2020 at 15:46):

Bringing that twitter energy to Zulip I see :)

Eduardo Ochs (Apr 25 2020 at 15:52):

GMT -4 is this, right?
https://www.timeanddate.com/worldclock/uk/greenwich-city
I missed it, but I'll try to be present the next time...

Reid Barton (Apr 25 2020 at 15:55):

No, that's just GMT, except when it isn't, such as now.
The start time is ~1 hour from now.

Jake Gillberg (Apr 25 2020 at 15:58):

I solemnly swear to solely use UTC time in the future. The start time is indeed ~1hr from now

Eduardo Ochs (Apr 25 2020 at 16:09):

Great! I'll be there!

Jake Gillberg (Apr 25 2020 at 16:56):

https://us02web.zoom.us/j/6853551826

Luc Chabassier (Apr 25 2020 at 21:50):

Thanks everyone. Can you post the links for the idris library here ?

Jake Gillberg (Apr 25 2020 at 23:22):

Library that we are working with: https://github.com/statebox/idris-ct/

Jake Gillberg (Apr 25 2020 at 23:23):

My messy hackings towards Idris as a Cartesian category: https://gitlab.com/jake.gillberg/programmingcats/-/blob/master/src/ProgrammingCats/MonoidalCategory/CartesianCategory.idr

Jake Gillberg (Apr 28 2020 at 00:29):

A WIP pull request implementing Cartesian Monoidal Categories: https://github.com/statebox/idris-ct/pull/81

Fabrizio Genovese (Apr 28 2020 at 00:32):

Jake Gillberg said:

A WIP pull request implementing Cartesian Monoidal Categories: https://github.com/statebox/idris-ct/pull/81

Cheers! We'll take a look asap!

Jake Gillberg (Apr 28 2020 at 00:34):

Still in progress! and @marcosh has been awesome at prompt replies / merging of completed work. I'm currently butting my head against the long / ?infinite? compile times of Monoidal Categories.

Fabrizio Genovese (Apr 28 2020 at 00:35):

Yes, so we know for sure that symmetric monoidal categories do not compile

Fabrizio Genovese (Apr 28 2020 at 00:35):

There's an open issue about that. Non symmetric ones work but compiling takes ages

Jake Gillberg (Apr 28 2020 at 00:36):

Do you know if the issue with symmetric monoidal categories would also be an issue with cartesian ones?

Fabrizio Genovese (Apr 28 2020 at 00:36):

Anyway we worked hard in the past to prove this, also together with @Andre Knispel . This is the main reason why we formalized products, terminal objects etc. We figured that proving that idris types and functions had products and terminal objects and use this to get a monoidal structure was better/nicer than doing it directly, but then we stopped

Fabrizio Genovese (Apr 28 2020 at 00:37):

Jake Gillberg said:

Do you know if the issue with symmetric monoidal categories would also be an issue with cartesian ones?

I really don't know. This bug is rather mysterious and if I recall correctly we weren't able to spot what made compiling fail when introducing symmetries. We are very much sure it's an Idris bug but it was very difficult to produce a minimal example

Jake Gillberg (Apr 28 2020 at 00:37):

Cool, yeah, I saw a bit of discussion on that and tried to pick up the work

Fabrizio Genovese (Apr 28 2020 at 00:38):

There are related open issues also on the idris repo

Jake Gillberg (Apr 28 2020 at 00:40):

Any attempts to get symmetric monoidal categories to compile in idris2?

Jake Gillberg (Apr 28 2020 at 00:44):

Ah, I see that at least as of late July there were some issues: https://github.com/statebox/idris-ct/issues/6#issuecomment-515981734

"Adding unitCoherence to MonoidalCategory.SymmetricMonoidalCategory causes the compiler to crash with Segmentation fault (core dumped)."

Christian Williams (Apr 28 2020 at 04:37):

I'm currently building idris-ct. Is it normal for it to take more than 5 or 10 minutes? Never built with Nix before.

Christian Williams (Apr 28 2020 at 04:46):

Okay, I assumed that the nix-build command would build the files in the current directory, so I didn't pass it an argument. It seems like it's just building tons of stuff... ah wait, it finally got to idris-ct. Lots of requirements, I guess.

Christian Williams (Apr 28 2020 at 05:02):

Type checking ./Discrete/DiscreteFunctor.lidr
Type checking ./Unit/UnitCategory.lidr
Type checking ./Comma/OverCategory.lidr
Type checking ./Comma/UnderCategory.lidr
Type checking ./Monad/Monad.lidr
/nix/store/7whxa62xjyfylxhww5w9ppjpsl4x9rim-stdenv-linux/setup: line 1332: 680 Killed idris --build idris-ct.ipkg
builder for '/nix/store/k4kyl0ncbx39gq88rvb7bfdnc15a0jpv-idris-idris-ct-dev.drv' failed with exit code 137
error: build of '/nix/store/gsks1avjndm1hidlqgpf18ajx059r0zf-idris-ct-doc-dev.drv', '/nix/store/k4kyl0ncbx39gq88rvb7bfdnc15a0jpv-idris-idris-ct-dev.drv' failed

So close. I'll try again tomorrow. (If anyone has advice let me know.)

sarahzrf (Apr 28 2020 at 05:46):

welcome to nix

sarahzrf (Apr 28 2020 at 05:46):

enjoy the deep end

Fabrizio Genovese (Apr 28 2020 at 09:55):

Christian Williams said:

I'm currently building idris-ct. Is it normal for it to take more than 5 or 10 minutes? Never built with Nix before.

If you want to build _everything_ it will probably take a couple of hours!

croy (May 01 2020 at 08:33):

Jake Gillberg said:

A couple of friends (of mostly programming and some maths background) are planning to read "Physics, Topology, Logic and Computation:A Rosetta Stone" and do some poking in Idris to guide our understanding. We plan to look over these overview slides / notes (http://math.ucr.edu/~mike/rosettaslides.pdf), (http://math.ucr.edu/~mike/rosetta%20slides.txt), read through section 2.4 of the paper, and meet next Saturday at 1:00 (GMT -4) to discuss

This group sounds cool! Is it on again tomorrow? What's been covered so far?

Jake Gillberg (May 01 2020 at 12:07):

@croy Yup! We are on for tomorrow at 17 UTC. We plan to start with a 30 min intro to Idris then discuss section 2.6 (closed categories). Last week we took a look at the statebox idris-ct library, and have made a bit of headway implementing cartesian categories.

Fabrizio Genovese (May 01 2020 at 12:09):

I may try to join if you want, I'm familiar with idris-ct more or less

Fabrizio Genovese (May 01 2020 at 12:09):

I could also spread the word in our internal chat, so that you can have some of our devs around if you need help with idris-ct :slight_smile:

Fabrizio Genovese (May 01 2020 at 12:10):

Would that be useful?

Jake Gillberg (May 01 2020 at 12:12):

Sure! If there is interest! I'd also be quite happy with some interaction through comments on the pull request

a13ph (May 01 2020 at 12:15):

@Jake Gillberg Would joining just to listen-in be okay? I'm playing catch-up :slight_smile:

Jake Gillberg (May 01 2020 at 12:16):

Yeah, not a problem! Happy to discuss previous material as well

a13ph (May 01 2020 at 12:21):

@Jake Gillberg Thanks. :blush: Wanted to make sure, since some groups are discouraging that, I think.
Regarding previous material - if I'll think I can ask a coherent question. I'll definitely try, but probably not in the first few sessions. Being on this Zulip is already a lesson in humility :joy:

Fabrizio Genovese (May 01 2020 at 12:26):

Jake Gillberg said:

Sure! If there is interest! I'd also be quite happy with some interaction through comments on the pull request

Cool! So there's a link or something?

Jake Gillberg (May 01 2020 at 12:26):

Fabrizio Genovese said:

Jake Gillberg said:

Sure! If there is interest! I'd also be quite happy with some interaction through comments on the pull request

Cool! So there's a link or something?

https://github.com/statebox/idris-ct/pull/81 . I've highlighted the point at which I am struggling in the comments

Jake Gillberg (May 01 2020 at 12:28):

a13ph said:

Jake Gillberg Thanks. :blush: Wanted to make sure, since some groups are discouraging that, I think.
Regarding previous material - if I'll think I can ask a coherent question. I'll definitely try, but probably not in the first few sessions. Being on this Zulip is already a lesson in humility :joy:

Agreed! I won't speak for everyone in the group, but I'd definitely call myself a beginner. Feel free to bring those incoherent questions, maybe we can turn them into coherent ones together :)

Fabrizio Genovese (May 01 2020 at 12:30):

Jake Gillberg said:

Fabrizio Genovese said:

Jake Gillberg said:

Sure! If there is interest! I'd also be quite happy with some interaction through comments on the pull request

Cool! So there's a link or something?

https://github.com/statebox/idris-ct/pull/81 . I've highlighted the point at which I am struggling in the comments

I mean, is there a link to the group chat/call?

Fabrizio Genovese (May 01 2020 at 12:31):

If I have to spread the word to our Devs in case they wanna chime in I got to tell them where they have to chime in xD

Jake Gillberg (May 01 2020 at 12:33):

... link to the group chat/call

ah, sure! https://zoom.us/j/6853551826 Sat: 17 UTC (starting with 30 min basic Idris intro, then moving on to closed categories and idris-ct

Jake Gillberg (May 02 2020 at 16:38):

A couple of us are in the room now! https://zoom.us/j/6853551826

Fabrizio Genovese (May 02 2020 at 16:52):

Cool!

a13ph (May 02 2020 at 18:10):

Thanks to whomever gave the Mac Lane suggestion. I've been putting it off, fearing it would be too theoretical with not enough examples. Now that I know it's rich in examples, which I don't need to know all, but only some... Well, that's exactly what I need to grok much of intro CT, I think.

Fabrizio Genovese (May 03 2020 at 14:47):

I did! Yes people keep saying that MacLane is not good to learn and I found that to be the most limiting suggestion of my career.

Todd Trimble (May 03 2020 at 15:49):

Hear hear.

Fabrizio Genovese (May 03 2020 at 17:12):

Another important advice: Do not focus too much on MacLane's exercises. They are _notoriously_ difficult. Like, legend is that some of them were open problems when the book came out. So you shouldn't try too hard to solve them, or getting frustrated if you can't. They are not meant to be friendly :D

Ohad Kammar (May 04 2020 at 11:59):

Fabrizio Genovese said:

Another important advice: Do not focus too much on MacLane's exercises. They are _notoriously_ difficult. Like, legend is that some of them were open problems when the book came out.

Do you know which ones?
I've been working my way through them and: 1) half the material is in them, and 2) they are great.

I do remember on exercise I got really stuck on, asking to come up with a counter example in presheaf categories, but I put it aside for a few years, and when I picked it up again it was immediate (taking the empty category as a counter-example)

Todd Trimble (May 04 2020 at 12:27):

I'd be interested to know myself; I don't know of any that could be considered open questions at the time of writing the first edition, not even close. However, I do remember one that made me throw up my hands when I first saw it (when I was pretty young)... well, it was from the first edition and I can't find either edition in my home library at the moment, but it had to do with all bracketings of monoidal products of $n+2$ indeterminates and associativities between them as forming a subdivision of the $n$-sphere. By now enough people know about associahedra that this problem might not seem so difficult anymore (and maybe his formulation was a bit imprecise), but at the time I first read it, it just seemed impossible.

Fabrizio Genovese (May 04 2020 at 16:53):

Well, I said "legend is that" because this is something that someone (don't remember who) told me during my PhD. I have no way to substantiate this claim. In any case, MacLane exercises are harder compared with other CT books, I thought this was something worth pointing out :slight_smile:

Jake Gillberg (May 04 2020 at 19:41):

Concerning the associator in a monoidal category, what are the source and target categories of the functors that make up the natural isomorphism? I'm still a bit tripped up by this after more thought

Nathanael Arkor (May 04 2020 at 19:48):

There's some choice. If you're happy using an unbiased cartesian product of categories, then you can take functors $\mathbb C^3 \to \mathbb C$ mapping $(X, Y, Z) \mapsto (X \otimes Y) \otimes Z$ and $(X, Y, Z) \mapsto X \otimes (Y \otimes Z)$.

Nathanael Arkor (May 04 2020 at 19:49):

If you want to use a binary cartesian product, then you need to reassociate in $\mathbf{Cat}$ using the pairing maps.

John Baez (May 04 2020 at 19:52):

Here $\mathbb{C}$ is your monoidal category, not the complex numbers. This should be obvious, but I never ever use $\mathbb{C}$ for anything except the complex numbers, so I momentarily thought Nathanael had gone mad. :upside_down:

Jake Gillberg (May 04 2020 at 19:58):

Ah great, unbiased cartesian product of categories looks like the definition given in nlab. I had only seen the binary version before. What does "reassociate in Cat" mean? The functors are endofunctors in cat?

Nathanael Arkor (May 04 2020 at 20:03):

You can define the functors instead $(\mathbb C \times \mathbb C) \times \mathbb C \to \mathbb C$, where one is given by $\otimes \circ (\otimes \times \mathrm{Id})$, and the other by $\otimes \circ (\mathrm{Id} \times \otimes) \circ \alpha_{\mathbb C}$, where $\alpha_{\mathbb C} : (\mathbb C \times \mathbb C) \times \mathbb C \to \mathbb C \times (\mathbb C \times \mathbb C)$ is given by re-pairing, using the universal property of the cartesian product.

Nathanael Arkor (May 04 2020 at 20:06):

(Here, $\alpha$ is the associator in the cartesian-monoidal category $\mathbf{Cat}$.)

Jake Gillberg (May 04 2020 at 20:12):

$\circ$ being functor composition? $\alpha_{\mathbb C}$ is the associator? Doesn't that put us right back where we started?

Nathanael Arkor (May 04 2020 at 20:14):

Yes, $\circ$ is functor composition. $\alpha$ is an associator in $\mathbf{Cat}$, but you don't need to know that to define a monoidal category. You're trying to define the associator in $\mathbb C$.

Nathanael Arkor (May 04 2020 at 20:14):

After you've defined a monoidal category, you can show that $\alpha$ happens to be the associator in a large monoidal category, but that's not necessary to define it in the first place.

Jake Gillberg (May 04 2020 at 20:19):

Ah, thanks! This helps a lot! I was misreading $\mathbf{Cat}$ as a synonym for $\mathbb C$ instead of the product of Categories and Functors. (the name for $\mathbb C$ in the idris-ct library that I am looking at is cat)

Nathanael Arkor (May 04 2020 at 20:21):

Sorry, I should have been clear about that. $\mathbb C$ is any small category here.

John Baez (May 05 2020 at 05:38):

This is an example of the "microcosm principle". We need the product in $\mathbf{Cat}$ to write down the tensor product in a monoidal category $\mathsf{C}$:

$\otimes : \mathsf{C} \times \mathsf{C} \to \mathsf{C}$

and similarly we need the associator in $\mathbf{Cat}$ to write down the associator in $\mathsf{C}$.

It keeps on going like this: if $\mathsf{C}$ is symmetric, we need the symmetry in $\mathbf{Cat}$ to write down the symmetry in $\mathsf{C}$, and so on. "Little things like to live in similar-shaped big things."

Jake Gillberg (May 06 2020 at 11:48):

Let's meet at the same time (17 UTC this Saturday) ready to discuss chapter 3

Jake Gillberg (May 09 2020 at 16:45):

https://zoom.us/j/6853551826 - I'm hanging out in here now if anyone wants to join, but we will get started in ~15 mins

a13ph (May 09 2020 at 18:23):

Various links from chat and today's discussion.
I might annotate how they connect to the topic or came up in discussion later.

We've discussed this Pull Request before recording
https://github.com/statebox/idris-ct/pull/83/files

Comparison of proof assistants
https://en.wikipedia.org/wiki/Proof_assistant#Comparison

Blog post by Dan Connoly about this reading group
https://www.madmode.com/2020/grok-idris-ct.html

Sequent calculus in Idris
https://gitlab.com/jake.gillberg/oplss-2019/-/blob/master/SequentCalculus.idr

Lambda-Calculus and Combinators: An Introduction -
by J. Roger Hindley, Jonathan P. Seldin
https://www.researchgate.net/publication/220688772_Introduction_to_Combinators_and_Lambda-Calculus

Computer science metanotation - given in various talks by Guy Steele
"It’s Time for a New Old Language" - https://www.youtube.com/watch?v=7HKbjYqqPPQ
some old slides - https://groups.csail.mit.edu/mac/users/gjs/6.945/readings/Steele-MIT-April-2017.pdf

a13ph (May 16 2020 at 11:41):

@Jake Gillberg are we continuing today? we still have Chapter 4 to go through

Jake Gillberg (May 16 2020 at 13:44):

My attention was diverted elsewhere this week, so I propose we take a week off and finish up the discussion next week. Thoughts?

a13ph (May 16 2020 at 14:50):

@Jake Gillberg I am personally okay with this, for myself.
For silent others too, seeing how there was no information in advance on whether there will be a session today.

a13ph (May 16 2020 at 15:13):

btw, in previous session, we had a discussion on dagger categories vs opposite categories. Here's a topic specifically about that: https://categorytheory.zulipchat.com/#narrow/stream/229199-learning.3A-basic.20questions/topic/Dagger.20categories/

croy (May 16 2020 at 15:49):

Chapter 4 for next week sounds good to me

croy (May 16 2020 at 15:57):

(and sorry for being one of the silent others)

Christian Williams (May 16 2020 at 17:02):

I plan to attend next time.

Luc Chabassier (May 28 2020 at 07:52):

Did you meet last saturday ? I couldn't attend... And is there a meeting planned this saturday ? Just checked there are only 4 chapters, so I guess the reading group is finished ^^'