Let being an isomorphism be a property

[EgbertRijke]

In this pull request I am testing out whether it is sensible to let isomorphisms be a property in a uniformly defined manner across the library.

Note: these changes are so far experimental, and I am unsure at the moment whether I actually want to propose to merge this line of thought.

[fredrik-bakke]

Hey! Although I don't know what your precise motivation is, I'm curious wouldn't a better setting be to consider this in a wild category without a class of equivalences? Then the framework will apply to structures that are not set-level, and we will additionally be able to avoid function extensionality (because of the setoid relation). To me, that sounds like a better definition.

[fredrik-bakke]

Of course, is-prop-iso will still rely on extensionality principles of the underlying type of morphisms, but many other constructions won't.