Explore what we want to call "isomorphisms"

[VojtechStep]

In #1056 (comment) @EgbertRijke raised the question whether we should keep with the type theory convention of having "isomorphisms" be in general maps with structure, or if we should reappropriate it for a well-behaved coherent concept.

For now we have the incoherent "isomorphisms in (large) (pre)categories" (invertible morphisms) and coherent "pointed isomorphisms" (biinvertible maps) are introduced in #1056.

[fredrik-bakke]

Hey! I'd just like to note that the notion of isomorphisms in precategories is not incoherent. Rather, it is coherent, but the definition is only coherent for set-level structures and doesn't generalize to higher structures without modifications.