Isomorphism of Structures in Algebra

[JacquesCarette]

I was quite surprised when it was pointed out to me that https://github.com/agda/agda-stdlib/blob/master/src/Algebra/Morphism/Structures.agda defined isomorphism in terms of injectivity and surjectivity which are quite set-theoretic in nature. I was fully expecting the more 'algebraic' notion with left and right inverse homomorphisms instead?

It's also fascinating how we have Monos singled out, but not Epis.

[Taneb]

I made an issue for Epis a couple of months ago, #2037

[jamesmckinna]

It's a very good point though, and one I have failed to make before... despite my concerns to recast much of Algebra.* in arrow/homomorphism-theoretic terms...

But it's hard not to think, all the more so, that the structure of that hierarchy has, indeed, been structured (sic) around the objects of the various categories, rather than their morphisms, tout court...

[jamesmckinna]

Re: Monos... indeed we also typically want regular monos in a category of algebras, with Epi=Surjective otherwise (IIRC!?)... and we do (will!) want (𝓔,𝓜)-factorisation systems on such categories...