Span diagrams

[EgbertRijke]

This pull request contains the changes from #885 that don't touch synthetic-homotopy-theory or structured-types, except those changes that are necessary to make the library compile.

This PR contains the following changes:

• Disambigating between spans and span diagrams. The disambiguation is explained in the relevant files.
• Developing infrastructure for spans and span diagrams, with the goal of making it useful for pushouts.
• Add extensive informal explanations to all the new files and to relevant existing files.
• Change is-injective-map-equiv to is-injective-equiv, because I needed the fact that map-equiv is an injective map somewhere.
• Refactors binary type duality and generalises the handling of universes for some of the components of binary type duality. We note specifically by avoiding a proof by equivalence reasoning, it was a lot easier to get the underlying equivalences to do the expected thing. Proofs by equivalence reasoning are more suitable in proofs where the actual equivalence is of less importance, such as abstract proofs.
• A note on equivalence reasoning was added to foundation-core.equivalences.lagda.md to record the previous point on the website.
• During the development of Rebase infrastructure for pushouts to span diagrams #885 I have left a lot of {{#concept }} macros with unattributed Agda fields. The quickest way to clean that up was just to run through all places where the macro was used and see if there are any unattributed fields. So I did that throughout the library. This includes for files that I would otherwise not have touched, because it didn't make sense to break up my workflow just for them.

Thanks for @VojtechStep for the idea of breaking down #885 into smaller pull requests.

[EgbertRijke]

I had to make some minimal changes to files in synthetic-homotopy-theory to make this branch compile.

[EgbertRijke]

I will self-review it before marking it as ready for review, but I think it compiles now.

[EgbertRijke]

I have done everything I wanted to do in this pull request, so it is now ready for review.

[EgbertRijke]

No rush, I am totally fine again on the other branch

[EgbertRijke]

I think this PR is done now

[fredrik-bakke]

Great! I can review the changes tonight most likely

[fredrik-bakke]

Holy crap, that was a lot of work done really quickly. Nice job!

[EgbertRijke]

Thanks for catching the typos!

[fredrik-bakke]

Merging now 🎉