English
There is an equivalence between functions of two arguments and functions with swapped arguments, given by swapping the two inputs.
Русский
Существует эквивалентность между функциями двух аргументов и функциями с поменянными аргументами, задаваемая перестановкой аргументов.
LaTeX
$$$$ (\\forall a,b, \\varphi(a,b)) \\simeq (\\forall b,a, \\varphi(a,b)). $$$$
Lean4
/-- Given `φ : α → β → Sort*`, we have an equivalence between `∀ a b, φ a b` and `∀ b a, φ a b`.
This is `Function.swap` as an `Equiv`. -/
@[simps apply]
def piComm (φ : α → β → Sort*) : (∀ a b, φ a b) ≃ ∀ b a, φ a b :=
⟨swap, swap, fun _ => rfl, fun _ => rfl⟩
