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.

[fredrik-bakke]

Considering that morphism types in a category are sets, I'd propose we rather use the following definition

Σ ( hom-Precategory C y x)
    ( λ g →
      ( comp-hom-Precategory C f g ＝ⁱ id-hom-Precategory C) ×
      ( comp-hom-Precategory C g f ＝ⁱ id-hom-Precategory C))

for isomorphisms, as this type has a strictly involutive inverse operator. In fact, it would be even better to use the pairing trick that Anders showed us (I'm sorry, this means backtracking on my initiative to use the strictly involutive identity type in set-level category theory), as that definition is predicative, something that might be important for large categories. The only caveat being that it only works for set-level things.

[fredrik-bakke]

@EgbertRijke This PR seems to have been abandoned. Maybe you'd want to open an issue on this question instead? I'd like to have the changes that are not about invertible morphisms in this PR merged if we can, without tackling the problem on how to define isomorphisms. That's for a different refactoring PR.

[fredrik-bakke]

There's also a question on whether we prefer the terminology section/retraction vs split epi/split mono in category theory.