prove various things are propositions

[emilyriehl]

We now have various logically equivalent definitions of is-prop here. It would be great to apply the various notions to prove that various types are propositions.

For instance, for any type A we can show that is-contr A implies is-prop A. A proof should be called is-prop-is-contr.

But also, for any type A, whether or not is-contr A holds, is-prop (is-contr A), i.e., is-contr A is a proposition. The agda-unimath library calls this is-property-is-contr.

Again for any f : A -> B, is-equiv A B f is a proposition. This might be called is-property-is-equiv.

There are lots of other types we should be able to prove are properties, in both the HoTT and sHoTT libraries, but let's start with just a few to settle on good style.

[emilyriehl]

@floverity may be interested in helping with this :)

[floverity]

Thanks! I'm keen to work on this.

[emilyriehl]

Hey @floverity just to let you know I could use is-property-is-equiv in particular ;)