In the first case:
- the top-level module parameters bind
A : Set a and B : Set b explicitly
- and then defines
Homomorphic₂ taking explicit arguments (_∼₁_ : Rel A ℓ₁) and (_∼₂_ : Rel B ℓ₂)
It seems 'obvious' that A and B could be given implicitly instead (but: breaking!), moreover that Homomorphic₂ could be given by delegation to f Preserves _∼₁_ ⟶ _∼₂_ from Relation.Binary.CoreFunction.Definitions.Congruent.
Indeed, that the whole module-level parametrisation could be rejigged using variables to streamline things more smoothly? module could be left as a stub, purely for compatibility cf. #1206 / #1213 . UPDATED: see #2922
In the second case:
- the top-level module parameters bind
A : Set a and B : Set b explicitly, together with (_∼₂_ : Rel B ℓ₂)
- and then defines
Homomorphic₂ taking explicit argument (f : A → B) (and the binary operations)
It seems 'obvious' here that B at least could be given implicitly instead (but: breaking!).
Are these 'bugs'/design decisions worth fixing?
Consequences:
- harmless within
stdlib in the deployment contexts for Algebra.Morphism.Definitions (but: knock-ons need fixing!)
- possibly more radical for
Relation.Binary.Morphism.Definitions but could be an improvement (avoid supplying 'bogus' explicit arguments A, B anywhere on qualified instantiated import...?)
In the first case:
A : Set aandB : Set bexplicitlyHomomorphic₂taking explicit arguments(_∼₁_ : Rel A ℓ₁)and(_∼₂_ : Rel B ℓ₂)It seems 'obvious' that
AandBcould be given implicitly instead (but:breaking!), moreover thatHomomorphic₂could be given by delegation tof Preserves _∼₁_ ⟶ _∼₂_fromRelation.Binary.CoreFunction.Definitions.Congruent.Indeed, that the whole
module-level parametrisation could be rejigged usingmodule could be left as a stub, purely for compatibility cf. #1206 / #1213 . UPDATED: see #2922variables to streamline things more smoothly?In the second case:
A : Set aandB : Set bexplicitly, together with(_∼₂_ : Rel B ℓ₂)Homomorphic₂taking explicit argument(f : A → B)(and the binary operations)It seems 'obvious' here that
Bat least could be given implicitly instead (but:breaking!).Are these 'bugs'/design decisions worth fixing?
Consequences:
stdlibin the deployment contexts forAlgebra.Morphism.Definitions(but: knock-ons need fixing!)Relation.Binary.Morphism.Definitionsbut could be an improvement (avoid supplying 'bogus' explicit argumentsA,Banywhere on qualified instantiated import...?)