The simplex precategory

[fredrik-bakke]

Define the simplex precategory and precategories of various posets.

[fredrik-bakke]

I'm not particularly happy with the current definition of the simplex category, so any advice on that is much appreciated. Also, I'd like to define simplicial sets for the purpose of defining quasi-categories, but category-theory does not seem like the proper place for that. Should a homotopy-theory module be made?

[EgbertRijke]

Awesome pull request!

[EgbertRijke]

I'm not particularly happy with the current definition of the simplex category, so any advice on that is much appreciated. Also, I'd like to define simplicial sets for the purpose of defining quasi-categories, but category-theory does not seem like the proper place for that. Should a homotopy-theory module be made?

Yes, that could be. I would call that folder simplicial-homotopy-theory, because a homotopy-theory folder would also contain Quillen model categories and so on, but it would probably be too much to have that all under one umbrella.

[fredrik-bakke]

Alright, I consider this a good stopping point for the PR. I'm aware that the file on inhabited finite total orders should be refactored a little. Ideally, one would perhaps want to have files all the way down to inhabited preorders, but that will be left for someone with more patience. Also, the files on different subprecategories of the precategory of posets should probably just become files about sub_categories_ once we have the proper theory established.

[EgbertRijke]

Excellent! I will review this in the evening

[EgbertRijke]

Beautiful PR! I will merge it when you update it.

(I don't want to be listed as coauthor merely for having merged the branch with master)

[fredrik-bakke]

I see. I wouldn't have minded to be honest, but now that we assign credit on the website, maybe we should be more strict about this? It's kinda sad that this restricts when we should use suggestions though. It really helps the review process.

[EgbertRijke]

I think it's ok for suggestions.