Surjections should be clarified as being split surjections

[mietek]

Could we have some clarifying comments added to the stdlib about the definition of surjection actually being the definition of split surjection? It would be helpful to people such as myself that continue to have trouble with the overloading of meaning in mathematical discourse. Example:
http://web.archive.org/web/20211026191457/https://twitter.com/EscardoMartin/status/1453039001783439370

(Andrej Bauer) Your definition of surjective is incorrect. Surjectivity is not definable in pure MLTT. Martín Escardó's notes elaborate on this in a nice way.

(Martín Escardó) We can say a bit more: your definition gives the notion of split surjection, that is, a surjection f with a right inverse g (meaning that f after g is the identity function).

Such clarifying comments can be found in @nad’s work:
http://www.cse.chalmers.se/~nad/listings/equality/Surjection.html

As a side note, I love how the linked code clearly states the following definition. I challenge you to locate this definition in the stdlib.

Split-surjective :
  ∀ {a b} {A : Type a} {B : Type b} → (A → B) → Type (a ⊔ b)
Split-surjective f = ∀ y → ∃ λ x → f x ≡ y

[gallais]

I challenge you to locate this definition in the stdlib.

I looked at Function/, opened Function.Definitions and found that it
was re-exporting Surjective from Function.Definitions.Core2.

Surjective : ∀ {a} {A : Set a} → (A → B) → Set (a ⊔ b ⊔ ℓ₂)
Surjective f = ∀ y → ∃ λ x → f x ≈₂ y

Granted the definition is parametrised over the notion of equality for the
domain / codomain but it's fine to provide a generalisation IMO.

[mietek]

I looked at Function/, opened Function.Definitions and found that it was re-exporting Surjective from Function.Definitions.Core2.

Ah! Thank you. Unfortunately, I looked at Function.Surjection and found myself in a never-ending rabbit hole of setoids.

record Surjective {f₁ f₂ t₁ t₂}
                  {From : Setoid f₁ f₂} {To : Setoid t₁ t₂}
                  (to : From ⟶ To) :
                  Set (f₁ ⊔ f₂ ⊔ t₁ ⊔ t₂) where
  field
    from             : To ⟶ From
    right-inverse-of : from RightInverseOf to

_RightInverseOf_ :
  ∀ {f₁ f₂ t₁ t₂} {From : Setoid f₁ f₂} {To : Setoid t₁ t₂} →
  To ⟶ From → From ⟶ To → Set _
f RightInverseOf g = g LeftInverseOf f

_LeftInverseOf_ :
  ∀ {f₁ f₂ t₁ t₂} {From : Setoid f₁ f₂} {To : Setoid t₁ t₂} →
  To ⟶ From → From ⟶ To → Set _
_LeftInverseOf_ {From = From} f g = ∀ x → f ⟨$⟩ (g ⟨$⟩ x) ≈ x
  where open Setoid From

This raises an important question that I am not qualified to answer. Is the setoid-based definition of Surjective named accurately, or not? See discussion:
https://twitter.com/EscardoMartin/status/1453074532726722571

[laMudri]

This raises an important question that I am not qualified to answer. Is the setoid-based definition of Surjective named accurately, or not?

I think not. In standard mathematical notation (i.e, ∃ means mere existence), we have:

• Surjective f = ∀y. ∃x. f x = y
• SplitSurjective f = ∃g. ∀y. f(g y) = y

Only the latter can yield a setoid morphism (standardly: function), which is what the above definition does. Incidentally, the mere existence of g would only appear if we were to form a setoid of proofs of SplitSurjective f. To reflect this, we would have all elements of SplitSurjective f be equal – i.e, the setoid is actually a proposition.

[laMudri]

Here are Andrej's definitions of surjective and epi on setoids, which agree with what I said.

[MatthewDaggitt]

So concretely @laMudri, what would you advocate changing our definitions to? See also the very bottom of this outstanding PR for changes to the definition of Surjective which I'd also like to merge in for v2.0:

https://github.com/agda/agda-stdlib/pull/1156/files

[laMudri]

In the non-setoid (_≡_) case, it's not clear to me that it makes sense to distinguish between surjective and split-surjective. We can't even state the distinction in MLTT.

In the setoid case, there is a distinction, and also conventional nomenclature for it. In Agda, these become:

• Surjective f = ∀ y → ∃ \ x → f ⟨$⟩ x ≈ y
• SplitSurjective f = ∃ \ (g : B ⟶ A) → ∀ y → f ⟨$⟩ (g ⟨$⟩ y) ≈ y

So, the Surjective of Function.Surjection should be called SplitSurjective. I believe the Surjective of #1156 is correctly named, though I'd maybe double-check the role of z.

The key when it comes to Surjective is that there's no guarantee that the choice of x respects equivalence on ys. I suppose a minimal counterexample would be to let A be the Boolean setoid and B be a setoid with two points which are equivalent. Then, let f : A ⟶ B be the identity on the underlying types. There is a proof of Surjective f where x is chosen to be y, whereas this would be impossible for SplitSurjective because such a choice of x would not respect equivalence in B.

Also, epi (and mono) would be nice to have, together with Andrej's proofs.

[MatthewDaggitt]

Okay, so Function.Surjection is being deprecated in v2.0 anyway, so I wouldn't worry too much about that.

Isn't SplitSurjective equivalent to Surjective in standard Agda? Given Surjective you can get SplitSurjective by constructing g as the first projection of Surjective, and likewise given SplitSurjective you can get Surjective by applying g?

[laMudri]

g is a setoid morphism (probably it's unclear that the arrow is slightly longer!), so while you can reconstruct its action, that action doesn't necessarily preserve equivalence.

[mietek]

In the non-setoid (_≡_) case, it's not clear to me that it makes sense to distinguish between surjective and split-surjective. We can't even state the distinction in MLTT.

As I was led to believe, we can’t state surjective in MLTT; we can only state split-surjective. This is the entire reason why I bring up this issue.

Okay, so Function.Surjection is being deprecated in v2.0 anyway, so I wouldn't worry too much about that.

This issue still applies to Function.Definitions.

[laMudri]

I had a look back at this issue, and AFAICS, the new Function hierarchy (Function.Bundles) uses a correct definition of surjection. I think split surjections are captured by LeftInverse. Therefore, I think this issue can be closed (though, it might be worth spinning off issues to document LeftInverse and make clear the relation to Surjection).

[dolio]

There is a weaker notion of surjectivity in plain MLTT. It is "epic" from category theory:

Epic f = ∀{l} {C : Set l} (g h : B -> C) -> (∀ a -> g (f a) ≡ h (f a)) -> (∀ b -> g b ≡ h b)

If you are thinking of types being set-like, then this is closer to surjectivity because you cannot recover a splitting from it. You can't actually prove that it's equivalent to a proper notion of surjectivity without something like propositional extensionality, though, I think (and of course, some sort of truncation to properly model surjectivity).

If you are thinking of types being like spaces, you need to augment it by adding that B and C are both homotopy sets. That is the one that is equivalent to "surjective" there, I think. (My personal theory is that there's a computational homotopy model where the unrestricted Epic above is also split-surjective, but I've heard there are classical counterexamples.)

Of course, this has the annoyance of being really large, because of being level polymorphic. You don't have to do that, but if you don't, I think you also won't be able to prove that it's equivalent to surjectivity (in the relevant scenarios) unless you have a small type of propositions (because one direction involves choosing C to be a type of propositions). Maybe induction-recursion can get you a small subset that is nevertheless sufficient, though (edit: it does appear you can do this).

[jamesmckinna]

Suggest closing this issue, after the merge of #1156, acknowledging the clash between Split offered here as a qualifier, and Strictly chosen there.

Sorry it's not always easy to keep track of all the cross-references between issues and PRs, especially when they haven't been explicitly (l)inked-in as such!