`flip` vs `Function.swap`

-- 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*.

Start by comparing flip in Init.Core with Function.swap in Mathlib.Logic.Function.Defs, then review the linked API counts for related uses. Decide which name and definition should remain, update the affected APIs consistently, and verify that the two functions are unified without changing their dependent-type behavior.