[DRY] Refactor algebraic properties of types

[jamesmckinna]

There's (a lot of) duplication between Function.Related.TypeIsomorphisms and Data.(Product|Sum).Algebra (and possibly elsewhere: eg the duplication of True↔ between the first of these, and Relation.Nullary.Decidable...).

This might be bad enough to want to deprecate whole modules, but there is a subtle problem exposed by #2419 , namely that not all the lemmas are as level-polymorphic as they might be, esp. those in Data.Product.Algebra, where the use of Algebra.Definitions imposes a homogeneous level restriction.

So a refined refactoring might be to makeFunction.Related.TypeIsomorphisms home for the heterogeneous level-polymorphic definitions (the direction in #2419 ), while making Data.*.Algebra home for the homogeneous/algebraic versions?

This feels as though it might be a useful clean-up, but potentially breaking wrt possibly unresolved Level metas and/or name clashing which no obvious (or at least: sensible) deprecation strategy can comfortably accommodate... cf #2421

[JacquesCarette]

Function.Related.TypeIsomorphism is both quite old and very useful. The level polymorphism is definitely something worth having.

I wonder if the (deeper) issue is that type "algebra" isn't quite 1-sorted algebra. So that our current Data.*.Algebra is correct wrt the usual notion of 'algebra', but we're encountering a genuine generalization here.

[jamesmckinna]

Function.Related.TypeIsomorphism is both quite old and very useful. The level polymorphism is definitely something worth having.

I agree (re: level polymorphism... but where these things live is moot, AFAIAC)

[jamesmckinna]

I wonder if the (deeper) issue is that type "algebra" isn't quite 1-sorted algebra. So that our current Data.*.Algebra is correct wrt the usual notion of 'algebra', but we're encountering a genuine generalization here.

I'm not sure I quite understand this: some things (esp. Level-polymorphic such) are 'large' notions (moreover: typically 'type constructors' in some form or another), whereas relative to a given carrier, the same things are 'small', and more like 'properties'/'structure'...? I was trying to cash that distinction out by saying we should... split them between different modules!?

[JacquesCarette]

If Agda had --cumulativity as default (which it doesn't, and I'm fine with that), one could see the stuff in Function.Related.TypeIsomorphism as 'algebra' for Set\omega.

In any case, it seems we agree: even though there is duplication, it should exist. Just elsewhere.