Shouldn't _≅_ be in Object? about agda-categories HOT 6 CLOSED

because it is really isormophism. the Iso predicate is really a bad name because that doesn't define isomorphism, but just mutual inverse relation between two morphisms.

from agda-categories.

It really is isomorphism of objects, I agree. It still feels like a construction over objects, as opposed to a property of morphisms...

but stdlib calls this Equivalence (between Setoids). It is in Function.Equivalence. Which actually goes some ways to convincing me that it does belong in Morphism. But you're right that Iso is not a good name. Equiv? Something else?

from agda-categories.

Equiv f g sounds like f and g are equivalent but it is not the case. probably Inverse?

I think it has something to do with how people think when perceiving Iso f g. people are thinking f and g together form an isomorphism, which is represented by A ≅ B containing both morphisms.

from agda-categories.

_≅_ is Inverse. stdlib uses InverseOf (which in our case would be indexed by 2 objects) for the current Iso. I'd be happy with that.

from agda-categories.

InverseOf indeed looks better.

from agda-categories.

After using this in other code, I've decided I'm actually fine with the name. Still not sure of the location, but it doesn't seem too bad, so let's call this moot.

from agda-categories.