[ refactor ] `Algebra.Morphism` wrt re-exports from `Algebra.Morphism.Definitions`

[jamesmckinna]

Reviewing #3034 made my head spin when I came (back) to Algebra.Morphism, the salient parts of which are given by

agda-stdlib/src/Algebra/Morphism.agda

Lines 24 to 31 in 7e77c5c

	------------------------------------------------------------------------
	-- Re-export
	module Definitions {a b ℓ₁} (A : Set a) (B : Set b) (_≈_ : Rel B ℓ₁) where
	open MorphismDefinitions A B _≈_ public
	open import Algebra.Morphism.Structures public

AFAICT, this re-export of Definitions acts solely to reparametrise the module Algebra.Morphism.Definitions in prenex form wrt its implicit arguments (and to 'rename' Definitions as ... Definitions!?)

Accordingly, suggest refactoring:

• to use variables in Algebra.Morphism.Definitions
• to handle the re-export in Algebra.Morphism as

  open import Algebra.Morphism.Definitions public as Definitions

• and to handle the knock-ons from these changes.

Unless there is something even-more-subtle I have failed to understand about module parameterisation!?

[JacquesCarette]

Perhaps a bit of git blame sleuthing to figure out who did this, and what the intent was? It sure seems mighty mysterious!

[jamesmckinna]

Shoutout to @MatthewDaggitt (for it was he... ;-)) to try to reconstruct what was going on in his brain of 7 years ago...

[MatthewDaggitt]

The answer is that I have no idea. Looking at that PR, there doesn't seem to be any point in that module declaration. We can just import it directly I think!