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!

[laMudri]

I don't think #1156 has anything to do with “split”, in the sense used in “split surjection”. The different definitions given in #1156 are all logically equivalent (assuming that the functions involved respect the (equivalence) relations), whereas surjections and split surjections are distinct in settings without choice.

[JacquesCarette]

Also, it would probably be nice to define @dolio 's Epic. I would be fine with opening a fresh issue and then closing this one?

[mietek]

The reason I opened this issue was that I found myself in a difficult spot in conversations, having called “a surjection” a mathematical object that my interlocutor considered to be merely “a split surjection”. To this end, I proposed not changing any of the definitions, but adding clarifying comments. It doesn’t seem to me that this issue has been resolved, because the definitions remain unchanged and uncommented. If the maintainers are fine with that, please mark this issue as “won’t fix” and close it.

[laMudri]

It's probably “won't fix” in the sense that the old Function hierarchy won't be fixed (because it will be deprecated), but is already fixed (IIRC) in the new Function hierarchy.

[mietek]

Please provide a link to the relevant portion of the new Function hierarchy.

[laMudri]

Surjection; LeftInverse = split surjection. As per my previous comment, there could be some small improvements around LeftInverse, but the definitions are basically right.

[ncfavier]

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

But in agda-stdlib, ∃ means Σ. Is that where the confusion is coming from?

Surjection uses Surjective, which looks split to me.

[laMudri]

Yeah, it's a little bit subtle. I'm talking about the setoid-based definitions, which are best thought of as working in the MLTT model of a setoid type theory (or a fragment of HoTT). The fact that to⁻ does not necessarily respect equality corresponds to the presence of a propositional truncation on the ∃ in HoTT.

In HoTT notation, Surjective (f : A → B) = Πy : B. ∥ Σx : A. f x = y ∥. Assuming Surjective f, we can get to⁻ : B → ∥ A ∥. In the setoid model, to⁻ is an equality-respecting function from the setoid B to the setoid whose carrier set is that of A, but whose equality is the always-true relation. Therefore, the congruence part of to⁻ is trivial, and, in the model, it's effectively just a function from the carrier of B to the carrier of A which doesn't respect equality. The latter is exactly what's in the library.

[laMudri]

Yeah, let's say that someone (quite possibly me) takes what we've learnt from this thread and puts it into the library. The resulting PR will close this issue.

As for your second paragraph, can you expand on this argument that “the Agda function arrow is surjective”? I think it should be the case that surjectivity and split surjectivity coincide on setoids whose equivalence relation is propositional equality. In particular, functions out of the set B are equivalent to equivalence-preserving functions out of the setoid ≡.setoid B.

[mietek]

Sorry, that was incorrectly phrased, hence the deleted comment. It’s difficult for me to phrase my issue correctly. The best I can offer at this time is that the Agda standard library uses building blocks that may be easily misinterpreted to mean something they don’t, and hence could merit comments.

[dolio]

The issue, I think, is that this defines what it means for MLTT functions to be surjective as, "satisfies the definition of surjectivity stated in the theory of setoids and unfolded into Martin-löf type theory." Internal to the theory of setoids, every setoid whose equivalence is the underlying equality is projective as a setoid, yes.

However, it is dubious whether everyone working natively with Agda/MLTT would consider this a satisfying definition of "surjective." They might want to imagine that Agda is itself an internal language for some other model, not just a theory for building witnesses underlying a setoid model of some other type theory. MLTT is somewhat inadequate, in that there is not a nice way to state the proper meaning of surjectivity of a MLTT function (although maybe in Agda you can do something with Prop? I don't know). But you can axiomatize the missing pieces, for example, and then instantiating the setoid-based definition to propositional equality gives you a stronger property. And of course it is evidently stronger than Epic as I mentioned.

[laMudri]

The best I can offer at this time is that the Agda standard library uses building blocks that may be easily misinterpreted to mean something they don’t, and hence could merit comments.

Right, yeah. I suppose the behaviour I've learnt is to not take definitions in .Definitions files at face value. Therefore, I didn't notice this problem. Maybe users should be directed via comments to more structured modules.

[Blaisorblade]

It might also be useful to document, in Functions.Definitions, that the relations are intended to be setoid equivalences. (I don't know why this does not just pass setoids — I can imagine reasons). "s/equality/setoid equivalence/" might help? "Equality" is either wrong (in MLTT) or needs context somewhere (if readers are supposed to read this in terms of a setoid type theory model).

[jamesmckinna]

TL;DR: what (else?) is required to be able to close this issue now?

[JacquesCarette]

As far as I can see, the long comment that @laMudri added in #2054 addresses everything that can be in Agda. Seems like closing is fine.