Zulip Chat Archive

Stream: Is there code for X?

Topic: simplicial sets


view this post on Zulip Kenny Lau (Aug 02 2020 at 11:15):

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

view this post on Zulip Kenny Lau (Aug 02 2020 at 16:34):

Looks like #144 is the answer

view this post on Zulip Reid Barton (Aug 02 2020 at 16:40):

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

view this post on Zulip Kenny Lau (Aug 02 2020 at 16:40):

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

view this post on Zulip Kenny Lau (Aug 02 2020 at 16:41):

looks like so

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

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

view this post on Zulip Jalex Stark (Aug 04 2020 at 17:36):

woah gerby is pretty cool

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

view this post on Zulip 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: May 07 2021 at 22:14 UTC