(Displayed) Category Theory: Sections of displayed categories, Free Category 3.0 and UMPs are Props

[maxsnew]

More displayed category theory, this PR introduces

1. local and global sections of displayed categories. The idea here is that in the internal type theory of category theory categories are contexts, displayed categories are types and (global) sections of displayed categories are terms. I also added many combinators for constructing these and in the process cleaned up the module structure of the displayed category theory parts a bit.
2. As an example use of sections, I've included another free category construction, which uses an elimination principle implemented as constructing a section of any displayed category over the free category which interprets the generators. This has the nice benefit of only needing to define one manual recursion over the HIT (the eliminator) rather than two (recursor and induction principle). The new free category construction is parameterized by a Quiver rather than a Graph, which is better to use in defining free constructions (I'll have an example in an upcoming PR). I ported over the category solver to use this new free category construction but left the old one in as the functor solver uses it.
3. I also included a proof that in a univalent category that universal elements are a Prop, which involved proving univalence of a few category constructions.

[jpoiret]

Looks generally cool to me, except for the two above comments. I've not used the category solver and don't know much reflection code so can't comment on that part.

[jpoiret]

Ah, you might be missing Cubical.Categories.Displayed.Section!