SetRel: Examples don't show why `α → β → Prop` is worse than `SetRel α β`

[OrfeasLitos]

Two possible definitions for SetRel are discussed in the documentation. It is argued there that SetRel α β is better than α → β → Prop - two examples are given to justify why. I was however unable to see why these examples show that the α → β → Prop approach "cracks at the seams".

[metakunt]

There are many possible answers to this question. One that is very useful is that it enables dot notation.
You don't get that with α → β → Prop but you get that with SetRel.
I would that point alone consider it to be worth it.

[OrfeasLitos]

The dot notation would work with def SetRel (α β : Type*) := α → β → Prop as well, no?

[metakunt]

I'm not an expert in this topic but I think that you don't get completions from the Set.* namespace with your definition.

[metakunt]

Here is a very real example where SetRel is better

import Mathlib

variable (a: SetRel ℕ ℕ) (b : ℕ → ℕ → Prop)

#check a.cod 
#check b.cod

https://live.lean-lang.org/#codez=JYWwDg9gTgLgBAWQIYwBYBtgCMBQOBuSUwSW6ApnABRIBccAyuTAErnpyCohFwJTVZx63QEmEXOKIAKUCGB54AxAGNU5RQGs4SAHSKIAEzg4lK9XCw79QA

[OrfeasLitos]

How exactly is it better? Note that it's possible to define SetRel.cod just like it's defined now if SetRel were defined as abbrev SetRel (α β : Type*) := α → β → Prop.

[OrfeasLitos]

@chenson2018 do you know why exactly Set (α × β) was chosen over α → β → Prop? What are the specific advantages?

[chenson2018]

Some previous discussions can be found at:

• #mathlib4 > Changing `Rel` to `Set (α × β)`, to help uniform spaces
• the description of the PR that made this change: [Merged by Bors] - refactor: make Rel less see-through #25587

The gist is that having an abbrev for function type was a bit strange, and there are mathematical applications where Set is preferred. I personally feel a little bit was lost in fully removing the old version. In CSLib for instance, we really would like to talk about the (co)domain of a relation α → β → Prop, and so have restored some of this under the Relation namespace.