`flip` vs `Function.swap`

[Komyyy]

-- Defined in `Init.Core`
def flip {α β : Sort*} {γ : Sort*} (f : α → β → γ) : β → α → φ :=
  fun b a ↦ f a b

-- Defined in `Mathlib.Logic.Function.Defs`
abbrev Function.swap {α β : Sort*} {φ : α → β → Sort*} (f : Π x y, φ x y) : Π y x, φ x y :=
  fun y x ↦ f x y

These are almost the same, and both have a non-negligible number of related APIs(flip: 72, Function.swap: 165).
These should be unified.

Personally, I think these should be unified to flip, since it is defined in the core library, and Function.swap is easily confused with Prod.swap.

Updated: α and β in flip is Sort*, not Type*.

[SnirBroshi]

The core version is not dependent. Are you just suggesting a name change? Otherwise, this needs to be a core RFC to make flip dependent

[Komyyy]

I briefly checked the Loogle results for swap, and Equiv.piComm seems to be the only definition using a dependent function type.
For downstream projects, however, I would like to add the dependent version dflip.