[ refactor ] Function.Definitions and Function.Consequences?

[jamesmckinna]

Against #2514 , and continuing to think about #1436 etc., cf. #2318

I think that it might be more ergonomic to refactor Function.Definitions to separate out:

• those Definitions parametrised on two equality relations, which would now become top-level module parameters
• the Strictly* definitions, parametrised on a single equality relation, which I would move to a distinct new Function.Definitions.Strict module, again parametrised on the relation (and indeed, the relative importance of these definitions relative to the others has been discussed at length; it feels as though they are 'special', and not for 'everyday' use, except for the Propositional instantiation with _≡_ in Data.Nat.Properties etc.)
• knock-on consequences: Function.Consequences and Algebra.Definitions, where in particular, one can immediately instantiate the two relations with the underlying equality of the Algebra (this would be the ergonomic payoff): eg. rephrasing the Cancellative properties in terms of Injective etc. cf. Refactor Algebra.Consequences.*? #2502

Draft PR in preparation.

Potentially breaking, so probably v3.0, but in terms of the overall structure/design of stdlib, I think the shift in parameterisation would be 'harmless', although it might go against the grain of the existing import/dependency structure of Function?

[MatthewDaggitt]

This is exactly the structure we used to have but it didn't work because of the way that Agda handles transitive top-level parameters. Therefore we switched to the current design in a breaking change. Let me try and dig up the issue.

[MatthewDaggitt]

See

• Remove Algebra.Definitions.Core(1/2) #1970
• Strict inverses #1156

There's also an upstream issue on the Agda repo describing the underlying problem with top-level module parameters where if I remember correctly there was some debate about whether the current behaviour that caused this is a bug or a feature. However, I can't seem to find it....

[jamesmckinna]

Wow!?

So I think that the 'problem' (IIUC, the failure to 'strengthen' a definition to only mention those module parameters actually used) is solved by the separation I propose (namely that the non-Strictly* definitions move to a module with a different parametrisation).

[MatthewDaggitt]

So if I understand it correctly your proposal is go back to the old design, but fix the problem by not having the auxiliary modules re-exported by the top level Definitions module?

[jamesmckinna]

I'll post the PR #2567 ... hmm there's more to this than meets the eye, including some existing opportunities for [DRY] refactoring.

[jamesmckinna]

So, I suspect that this is now moot, given the larger-scale developments in #2568 / #2569 but I think may still be worthwhile downstream as part of tackling #2570 ... so marking as blocked-by-issue for the time being.

[jamesmckinna]

Additionally: the unsolved metas mentioned in #2566 largely seem to originate from Function.Consequences.Propositional, where

• strictlySurjective⇒surjective should have its argument f explicit to supply to cong
• strictlyInverseʳ⇒inverseʳ should have its argument f⁻¹ explicit (and not f), because it is precisely the formal dual of strictlyInverseˡ⇒inverseˡ, so (presumably!?) its quantification should reflect that...

These would each be breaking changes, though only wrt 2 imports/3 uses in the stdlib besides those tidied up by #2569 , viz.:

• Data/Fin/Properties.agda: open import Function.Consequences.Propositional using (contraInjective) (whose parametrisation is unaffected by the above changes, as it inherits directly from Setoid) (2 uses)
• Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda: open import Function.Consequences.Propositional using (strictlySurjective⇒surjective) (1 use)