Factor out standard pullbacks

[fredrik-bakke]

• Factors foundation(-core).pullbacks into a treatment for standard pullbacks in foundation(-core).standard-pullbacks, and cones satisfying is-pullback in foundation(-core).pullbacks. This makes the file about pullbacks much more readable, finally.
• Deletes foundation.pullback-squares because it was just a stub, and led to misuse in some places. After a refactoring of cones, we may want an additional file about pullback cones.

[fredrik-bakke]

I will review this PR myself a little later. In the meanwhile, since I believe it is close to done I will mark it as ready for review.

[fredrik-bakke]

I've marked this PR as ready for review again. I'll request a review specifically from Egbert, as he may have some objections to the refactor.

[fredrik-bakke]

Thank you for the review, it is most helpful!

[fredrik-bakke]

Your suggestions are very sensible, and I think they will heighten the quality of this refactoring substantially.

[fredrik-bakke]

We could perhaps consider doing a file about type arithmetic for standard pullbacks, recording such things as

• Commutativity of standard pullbacks
• Associativity of standard pullbacks given a ternary span
• Unit laws of standard pullbacks (when either leg is the identity)
• Zero laws of standard pullbacks when any of the types in the cospan are empty

[fredrik-bakke]

How's this?

[fredrik-bakke]

I've addressed your comments as best I can. Let me know if there is anything else to do or if this PR is ready for merging.

[fredrik-bakke]

I'm gonna go ahead and merge this PR as I need it to continue my work. If there are any future comments, I can fix them in a subsequent PR.