English
Let α, β, γ be types and let f be a symmetric function in its first two arguments and in its last two arguments, i.e. f a1 a2 b1 b2 = f a2 a1 b1 b2 and f a1 a2 b1 b2 = f a1 a2 b2 b1. Then for all a1,a2 ∈ α and b1,b2 ∈ β, the lifted value satisfies lift₂ f (s(a1,a2)) (s(b1,b2)) = f a1 a2 b1 b2.
Русский
Пусть α, β, γ — множества/типы. Пусть f: α × α × β × β → γ удовлетворяет симметрии по первым двум аргументам и по последним двум аргументам: f a1 a2 b1 b2 = f a2 a1 b1 b2 = f a1 a2 b2 b1. Тогда для любых a1,a2 ∈ α и b1,b2 ∈ β выполняется lift₂ f (s(a1,a2)) (s(b1,b2)) = f a1 a2 b1 b2.
LaTeX
$$$ \\operatorname{lift}_2 f\\, s(a_1,a_2)\\, s(b_1,b_2) = f(a_1,a_2,b_1,b_2). $$$
Lean4
@[simp]
theorem lift₂_mk
(f : { f : α → α → β → β → γ // ∀ a₁ a₂ b₁ b₂, f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁ })
(a₁ a₂ : α) (b₁ b₂ : β) : lift₂ f s(a₁, a₂) s(b₁, b₂) = (f : α → α → β → β → γ) a₁ a₂ b₁ b₂ :=
rfl
