Applications of Univalence

[maxsnew]

If C is a univalent category, then the type of universal elements of a presheaf on C should be a property. We now have an application of this in the cartesian product solver.

This should follow from proving that the category of elements of a presheaf on a univalent category is univalent, because we have already shown universal elements are equivalent to terminal objects on the category of elements, and terminal objects are already shown to be a prop.

Proving this is going to take some work though because there isn't much in cubical for working with univalent categories and because you run into transport hell pretty much immediately. The following properties look useful:

1. Transport along isoToPath in SET is equal to applying the function (the equivalent of uaβ in Foundations.Univalence).
2. If F is a functor whose domain and codomain are univalent, then isoToPath of F-iso F iso is equal to cong (F .F-ob) of isoToPath

And possibly more...

[maxsnew]

Completed in branch universal-element-prop. I'll merge in after the cubical changes PR is merged

[maxsnew]

Implemented in #40