English
The lift equivalence between symmetric two-argument functions and functions from Sym2 α to β.
Русский
Эквивалентность между симметричными функциями двух аргументов и функциями из Sym2 α в β.
LaTeX
$$$$ \text{lift} : \{ f : α \to α \to β \// \forall a_1 a_2, f a_1 a_2 = f a_2 a_1 \} \simeq (Sym2 α \to β). $$$$
Lean4
/-- The universal property of `Sym2`; symmetric functions of two arguments are equivalent to
functions from `Sym2`. Note that when `β` is `Prop`, it can sometimes be more convenient to use
`Sym2.fromRel` instead. -/
def lift : { f : α → α → β // ∀ a₁ a₂, f a₁ a₂ = f a₂ a₁ } ≃ (Sym2 α → β)
where
toFun
f :=
Quot.lift (uncurry ↑f) <| by
rintro _ _ ⟨⟩
exacts [rfl, f.prop _ _]
invFun F := ⟨curry (F ∘ Sym2.mk), fun _ _ => congr_arg F eq_swap⟩
right_inv _ := funext <| Sym2.ind fun _ _ => rfl
