Pushouts and pullbacks in categories

[ben-connors]

This PR standardizes pullbacks in category-theory with standard pullbacks in foundation and dualizes them to get pushouts matching pushouts in synthetic-homotopy-theory.

[ben-connors]

The current state is what was pulled from #1442, which needs a lot of work.

[ben-connors]

Regarding the switch to using span diagrams, should this also be done for pullbacks?

[fredrik-bakke]

Regarding the switch to using span diagrams, should this also be done for pullbacks?

Cospan diagrams, yes

[fredrik-bakke]

Note the distinction between the term "span" and "span diagram" in the library btw (check the corresponding definitions for types). However, in category-theory we also have access to the definition as a functor from the representing span diagram, I don't know what to do about that.

[ben-connors]

I've been running into this same question dealing with the arrow (pre)category. One really wants when dealing with these things to have the objects and morphisms to be literally the appropriate sigma type, since then you can use Agda's pattern matching directly. But for showing it was a category, it ended up being easiest to essentially establish an equivalence of precategories between it and the functor precategory from the representing arrow, though I suspect that's what you'd want to do anyways for showing that it actually "represents" morphisms. I have this in a very early form here:

https://github.com/ben-connors/agda-unimath/blob/9e866d48193e2545d1a2460ab9521d880500e727/src/category-theory/arrow-precategories.lagda.md

My opinion at the moment is that it's still best to define this all for (co)spans directly rather than functors out of the representing (co)span category, since functions in category-theory tend to collect so many garbage explicit arguments that pattern matching and the ability to just use projections directly can really cut down proof length at the cost of a bit more initial pain to establish the category structure.

[fredrik-bakke]

Thank you so much for doing this by the way!