## 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

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

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

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: May 07 2021 at 22:14 UTC