multicoequalizers in Type

Stream: PR reviews

[Joël Riou]

The following series of three PR allows to study certain colimits in Type. It will be important in order to show that in the category of simplicial sets, it will allow constructing morphisms from horns:

[Joël Riou]

• refactor(CategoryTheory/Limits): colimits in Type #25823

[Joël Riou]

• feat(Order): bicartesian squares in lattices #26037

[Joël Riou]

• feat: multicoequalizers in the category of types #26847

[Joël Riou]

(This will be used in the infinity cosmos project in order to construct the homotopy category of (truncated) quasicategories.)

[Robin Carlier]

Will try to have a second look at #25823 this evening.