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 https://github.com/agda/agda-stdlib/blob/f1368a6541aae6328159e6c8ea4eb7d40fe0c5d0/README.agda#L166-L168 . 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).

[MatthewDaggitt]

Modules that have functionality that needs to be transferred across:

Core functionality

A lot of stuff in these modules has been ported, but modules are not marked completed until all of it is has.

• [x] src/Function/Equality.agda
  • [x] Missing an indexed function variant. Should go in a new hierarchy Function.Dependent.(Structures/Bundles)
  • [x] setoid in Function.Indexed.Relation.Binary.Equality
  • [x] ≡-setoid
  • [x] flip
• [x] src/Function/Injection.agda
• [x] src/Function/Surjection.agda
  • [x] fromRightInverse (should probably go in a new module Function.Properties.RightInverse)
• [x] src/Function/Bijection.agda
• [x] src/Function/Inverse.agda
  • [x] _↔̇_ (what even is that weird character above the arrow?)
  • [x] fromBijection (should probably go in a new module Function.Properties.Bijection)
  • [ ] map (under some sort of Function.Construct.X module? Does this operation generalise to other function structures?)
  • [ ] zip (under some sort of Function.Construct.X module? Does this operation generalise to other function structures?)
• [x] src/Function/LeftInverse.agda
• [x] src/Function/HalfAdjointEquivalence (not even bundles/structures done yet)

Dependencies

Unless stated otherwise most of these are simply copying the definitions and updating them to use the new hierarhcy.

Easy

• [x] src/Algebra/Construct/LiftedChoice.agda
• [x] src/Data/List/Countdown.agda
• [x] src/Data/Fin/Properties.agda
• [x] src/Data/Nat/Properties.agda

Moderate

• [x] src/Data/List/Membership/Propositional/Properties.agda
• [x] src/Data/Product/Function/NonDependent/Setoid.agda
• [x] src/Data/Product/Relation/Binary/Pointwise/NonDependent.agda
• [x] src/Data/Product/Function/NonDependent/Propositional.agda
• [x] src/Data/Sum/Function/Setoid.agda
• [x] src/Data/Sum/Function/Propositional.agda
• [x] src/Relation/Nullary/Decidable.agda
• [x] src/Function/Related.agda (should be relatively simple, need to define alternative mappings for each kind)
• [x] src/Function/Related/TypeIsomorphisms (I think this has already been done by @JacquesCarette in Data.(Sum/Product).Algebra.)

Hard

Uses dependent functions, which we don't yet have a hierarchy for (see comment on Function.Equality above)

• [x] src/Data/Product/Function/Dependent/Setoid.agda
• [x] src/Data/Product/Function/Dependent/Setoid/WithK.agda
• [x] src/Data/Product/Function/Dependent/Propositional.agda
• [x] src/Data/Product/Function/Dependent/Propositional/WithK.agda

[JacquesCarette]

I've got two new summer students, and I've asked them to start their work on stdlib here. Expect PRs 'soon'.

[Saransh-cpp]

Hi! Glad to be here! Just to make sure I got this right -

agda-stdlib used to have a particular structure for the Function module (or package?) which wasn't very user friendly. This issue aims to restructure the module in such a way that the imports make more sense to the users and the developers.

So there are two sides here -

1. Migrating the actual code to a different location
2. Updating the Function imports or dependencies in other packages/modules

In a future major release, the following modules will disappear completely -

 Function.Equivalence
 Function.Equality
 Function.Bijection
 Function.Injection
 Function.Surjection
 Function.LeftInverse

and maybe even more.

If I did get this right, I am currently trying to migrate fromBijection from Function.Inverse to Function.Properties.Bijection. I am getting some errors while running the tests locally and I am debugging them at the moment. I might require some help in debugging the failures, will create a PR shortly with more information.

[JacquesCarette]

Yes, that's essentially correct. It's probably a good idea to start new issues for discussion of each sub-part (when needed), otherwise this issue is going to "blow up" in size (it's already quite long). Debugging help is definitely best asked for on Zulip and other messaging sites.

[Saransh-cpp]

Great! Thank you so much! I'll redirect all the debugging questions to Zulip or Discord.

[Saransh-cpp]

Based on some digging and a discussion on zulip, I think the following can be crossed off the list -

• fromRightInverse
• fromBijection

---

• src/Function/Related.agda
• src/Function/Surjection.agda
• ~src/Relation/Nullary/Decidable.agda~ maybe not this

[MatthewDaggitt]

Thanks @Saransh-cpp for the help! Feel free to cross them off if you find they're already done.

So I've got a PR open that does some of this already (https://github.com/agda/agda-stdlib/pull/1895). In particular:

• src/Data/Product/Function/Dependent/Setoid.agda
• src/Data/Product/Function/Dependent/Setoid/WithK.agda
• src/Data/Product/Function/Dependent/Propositional.agda
• src/Data/Product/Function/Dependent/Propositional/WithK.agda

However, it ended up blocked on https://github.com/agda/agda-stdlib/pull/1156. Hopefully that should be merged in sometime this week.