English
Elevate a binary type operation to an operation on cardinals; given a way to transport equivalences on the inputs to the outputs, one gets a lifted binary operation on cardinals.
Русский
Пусть дано бинарное преобразование типов, и есть способ переносить эквивалентности входов в эквивалентности выходов; тогда получаем возведённую в кардиналы бинарную операцию.
LaTeX
$$$\\mathrm{map}_2\\; (f:\\, \\text{Type}\\, u \\to \\text{Type}\\, v \\to \\text{Type}\\, w)\\; (hf:\\, \\forall \\alpha \\beta \\gamma \\delta, \\alpha \\simeq \\beta \\to \\gamma \\simeq \\delta \\to f\\alpha\\gamma \\simeq f\\beta\\delta) : \\text{Cardinal} \\to \\text{Cardinal} \\to \\text{Cardinal}$$$
Lean4
/-- Lift a binary operation `Type* → Type* → Type*` to a binary operation on `Cardinal`s. -/
def map₂ (f : Type u → Type v → Type w) (hf : ∀ α β γ δ, α ≃ β → γ ≃ δ → f α γ ≃ f β δ) :
Cardinal.{u} → Cardinal.{v} → Cardinal.{w} :=
Quotient.map₂ f fun α β ⟨e₁⟩ γ δ ⟨e₂⟩ => ⟨hf α β γ δ e₁ e₂⟩
