Zulip Chat Archive

Stream: Is there code for X?

Topic: simplicial sets

Kenny Lau (Aug 02 2020 at 11:15):

What's the progress of simplicial sets? @Johan Commelin @Reid Barton

Kenny Lau (Aug 02 2020 at 16:34):

Looks like #144 is the answer

Reid Barton (Aug 02 2020 at 16:40):

there's also https://github.com/leanprover-community/mathlib/commits/sset

Kenny Lau (Aug 02 2020 at 16:40):

oh, did @Johan Commelin forget about his old PR and restart?

Kenny Lau (Aug 02 2020 at 16:41):

looks like so

Reid Barton (Aug 02 2020 at 20:18):

I've also just started formalizing some stuff on simplicial sets, but I'm not using mathlib's category theory library

Reid Barton (Aug 04 2020 at 15:06):

By the way, it might go without saying but kerodon.net is the source I would recommend for simplicial sets.

Jalex Stark (Aug 04 2020 at 17:36):

woah gerby is pretty cool

Johan Commelin (Aug 07 2020 at 19:21):

Kenny Lau said:

oh, did Johan Commelin forget about his old PR and restart?

Yup, the old approach gave problems. Now I'm using the category of all nonempty finite linear orders, instead of a copy of nat. It seems to work better.

Johan Commelin (Aug 07 2020 at 19:21):

But I'll be on holidays for another week, so don't expect PRs soon.

Last updated: Dec 20 2023 at 11:08 UTC