English
Lifting commutes with composition: applying map g and then lifting f is the same as lifting the function that sends (c1,c2) to f(g c1,g c2).
Русский
Подъем (lift) коммутирует с отображением: сначала применяется map g, затем lift f, что эквивалентно подъему функции, отправляющей (c1,c2) в f(g c1, g c2).
LaTeX
$$$ \\mathrm{lift} \\ f \\circ \\mathrm{map} \\ g = \\mathrm{lift} \\langle \\text{fun }(c_1,c_2):\\gamma\\times\\gamma \\Rightarrow f(g\\,c_1, g\\,c_2), \\dots \\rangle. $$$
Lean4
theorem lift_comp_map {g : γ → α} (f : { f : α → α → β // ∀ a₁ a₂, f a₁ a₂ = f a₂ a₁ }) :
lift f ∘ map g = lift ⟨fun (c₁ c₂ : γ) => f.val (g c₁) (g c₂), fun _ _ => f.prop _ _⟩ :=
lift.symm_apply_eq.mp rfl
