Deprecate old function hierarchy

[mechvel]

I propose the following two backwards compatible additions.

(1) To add to Function.Injection

InjectiveBy≡ : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → Set _
InjectiveBy≡ f =  ∀ {x y} → f x ≡ f y → x ≡ y

To add to Function.Surjection

SurjectiveBy≡ : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → Set _
SurjectiveBy≡ {_} {_} {_} {B} f =  (y : B) → ∃ (\x → f x ≡ y)

To add to Function.Bijection

BijectiveBy≡ : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → Set _
BijectiveBy≡ f =  InjectiveBy≡ f × SurjectiveBy≡ f

(2) To reexport In(Sur,Bi)jective, In(Sur,Bi)jectiveBy≡ from Function.

Motivation.
(2) is proposed because it is nicer to write a single ... import Function using (...)
instead of the four import decls:
Function, Function.Injection, Function.Surjection, Function.Bijection.

(1) is proposed because In(Sur,Bi)jectiveBy≡ have a wide application area and also are simple to perceive and to use, while the generic In(Sur,Bi)jective are declared so that they are difficult to perceive and to use.
If the user really needs the general version, all right, let him study the general constructs given there by records.

[gallais]

The problem I can see with these definitions is that we would now have two
(essentially the same on propositional equality) distinct notions of injectivity
and we would need to convert between them.

We already have "smart constructors" for injectivity involving propositional
equality, would that solve your problem? https://agda.github.io/agda-stdlib/Function.Injection.html#1399

[mechvel]

For example, consider

suc-injective :  ∀ {m n} → suc m ≡ suc n → m ≡ n
suc-injective refl = refl

in Data.Nat.Properties. Why does not it use Injective ? Can you demonstrate the usage of smart constructors for suc-injective : Injective suc ?

Now, I suggest the following.

------------------------------------------------------------ Function/GenericInjSurBi.agda ---------
module Function.GenericInjSurBi where
...
module _ {ℓ ℓ= ℓ' ℓ'=} (From : Setoid ℓ ℓ=) (To : Setoid ℓ' ℓ'=)
  where
  open Setoid From using () renaming (Carrier to A; _≈_ to _≈_)
  open Setoid To     using () renaming (Carrier to B; _≈_ to _≈'_)

  GenericInjective : Pred (A → B) _
  GenericInjective f =  ∀ {x y} → f x ≈' f y → x ≈ y

  GenericSurjective : Pred (A → B) _
  GenericSurjective f =  (y : B) → ∃ (\x → f x ≈' y)

  GenericBijective : Pred (A → B) _
  GenericBijective f =  GenericInjective f × GenericSurjective f

module _ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'}
  where
  InjectiveBy≡ SurjectiveBy≡ BijectiveBy≡ :  Pred (A → B) _

  InjectiveBy≡  =  GenericInjective  (PE.setoid A) (PE.setoid B)
  SurjectiveBy≡ =  GenericSurjective (PE.setoid A) (PE.setoid B)
  BijectiveBy≡  =  GenericBijective  (PE.setoid A) (PE.setoid B)
-----------------------------------------------------------------------------------------------------------------

Example of usage: put to Data.Nat.Properties

open import Function.GenericInjSurBi using (InjectiveBy≡)    

suc-injective : InjectiveBy≡ suc 
suc-injective refl = refl

GenericInjective co-exists with Injective of lib-1.0 and also is more generic. Because if cf is a congruent map between setoids, then in can be derived
GenericInjective f for f : Carrier₁ → Carrier₂ extracted from cf -- probably it can be extracted.
(I never used Injective of lib-1.0 and do not know how is it arranged, and what constructors to use).

A similar relation is for Surjective and Bijective.
In most situations the users will use GenericIn(Sur,Bi)jective or In(Sur,Bi)jectiveBy≡.
In the remaining situations let them use In(Sur,Bi)jective by lib-1.0.
Also I would like to rename GenericInjective to Injective,
and to rename Injective of lib-1.0 to something -- if you can agree with this breaking backwards compatibility.

[MatthewDaggitt]

If anything should be done to the function hierarchy then it should be made more consistent with other record hierarchies (e.g. IsInjection/Injection). Obviously this is fairly non-backwards compatible. I'm currently not sure how this would interact with the current design of exposing the setoids directly.

I agree with @mechvel though that they should be exported by Function directly.

[mechvel]

Can you point concretely, may be with example: what harm can do using the above GenericInjective or InjectiveBy≡ ?
I have shown the advantage, now, please, show a drawback.

For any occasion: I am not in a hurry, I can wait long for people to return from holydays and to concentrate on the answer. I post things in the process, because if I delay the post, then I would deal with another subjects and probably forget of the issue.

[MatthewDaggitt]

Can you point concretely, may be with example: what harm can do using the above GenericInjective or InjectiveBy≡ ? I have shown the advantage, now, please, show a drawback.

The problem is one of long-term drawbacks rather than short-term drawbacks. The end goal should be to make the library consistent and therefore easy to use. At the moment the function hierarchy does not follow the same rules as the other hierarchies in the library, and this discourages users from using it, as you yourself said.

The problem with your proposal is that it would add further non-standard names that do not obey the IsX/X convention. This creates further work in the future when we get around to fixing the hierarchy. I agree with the problems you have identified, but I'm not sure your proposed solution is the right long-term way to go about fixing it.

I'm afraid tackling the function hierarchy isn't on anyone's immediate list of priorities at the moment as far as I'm aware, but I'll leave the issue open as a reminder.

[mechvel]

I'm afraid tackling the function hierarchy isn't on anyone's immediate list of priorities

I do not know precisely whether I am in the anyone list, but for any occasion, let me name my top priorities relatively to Standard.

1. The features named in the announcement of BFLib-0.1 and implemented there:
   generic definition of divisibility, gcd, generic fraction arithmetic, a full item set for Bin.
2. Certified arithmetic of natural numbers represented as lists of macro-digits.

What is function hierarchy? For example, are the matters of a generic definition of divisibility and gcd, generic definition of a fraction (see BFLib) of function hierarchy ?

As to GenericInjective, the proposals for standard can easily avoid this issue at all. For example, to write everywhere things like

  suc-injective :  ∀ {m n} → suc m ≡ suc n → m ≡ n
  foo-injective :  ∀ {x y} →  foo x ≈'  foo y →  x ≈ y
  

The result will be that no user would set the words Injective, Surjective, Bijective of standard to the type expressions.

[MatthewDaggitt]

What is function hierarchy? For example, are the matters of a generic definition of divisibility and gcd, generic definition of a fraction (see BFLib) of function hierarchy ?

See in README.agda

agda-stdlib/README.agda

Lines 166 to 168 in f1368a6

	------------------------------------------------------------------------
	-- Record hierarchies
	------------------------------------------------------------------------

.
The examples you give above are therefore not part of the function hierarchy.

As to GenericInjective, the proposals for standard can easily avoid this issue at all. For example, to write everywhere things like.
...
The result will be that no user would set the words Injective, Surjective, Bijective of standard to the type expressions.

As I said above, I agree it's a problem that there's no easy-to-use definitions for Injective, Surjective etc. in the library, but I don't think GenericInjective is the way to go. What I have in mind is:

module _ {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b} where

  Injective : Rel A ℓ₁ → Rel B ℓ₂ → (A → B) → Set _
  Injective _≈_ _≈′_ f = ∀ {x y} → f x ≈′ f y → x ≈ y

  record IsInjection (_≈_ : Rel A ℓ₁) (_≈′_ : Rel B ℓ₂)
                     (f : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
    field
      cong      : f Preserves _≈_ ⟶ _≈′_
      injective : Injective _≈_ _≈′_ f

  record Injection : Set (a ⊔ b ⊔ suc ℓ₁ ⊔ suc ℓ₂) where
    field
      _≈_         : Rel A ℓ₁
      _≈′_        : Rel B ℓ₂
      f           : A → B
      isInjection : IsInjection _≈_ _≈′_ f

This follows the same record hierarchy as in Algebra and Relation.Binary. The proof of injectivity could then be written as:

suc-injective : Injective _≡_ _≡_ suc
suc-injective refl = refl

Obviously what to do with the existing code is problematic. We could move them to a separate sub-directory Function.Setoid.

[mechvel]

This is better than Injective of lib-1.0. The drawback is pushed one level down.
The matter is that for a theory with equality injectivity has sense not only for congruent maps
(I can give a simple example), and its code is simpler to use.
The code will be nicer and more usable if the library delays as possible introducing the congruence condition. Say,

 Injection =   Σ (A → B) (Injective _≈_ _≈′_)

And the corresponding definitions for congruent maps can be obtained by joining the above definitions with the condition of Congruent f, with also inserting the "Cong" word somewhere to the name of the predicate.
(?)

Also it is desirable to avoid records for simple definitions (?)
-- because the field names usually cause the necessity of renaming. For example, this cong will clash with PropositionalEquality.cong, which creeps in almost everywhere.
If you call this field differently, then its meaning will not be so easily understood.

Similarly, _∣_ looks better and is used easier when it is defined as ∃ (\q → a ≈ q ∙ b).