English
There is a way to lift a map between Type-level objects to a map between Cardinal values, compatible with equivalences.
Русский
Существует способ перенести отображение между типами на отображение между кардиналами, сохраняющее эквивалентности.
LaTeX
$$$\\text{map} : (f:\\, \\text{Type}\\, u \\to \\text{Type}\\, v) \\to (\\forall \\alpha \\beta, \\alpha \\simeq \\beta \\to f\\alpha \\simeq f\\beta) \\to \\text{Cardinal} \\to \\text{Cardinal}$$$
Lean4
/-- Lift a function between `Type*`s to a function between `Cardinal`s. -/
def map (f : Type u → Type v) (hf : ∀ α β, α ≃ β → f α ≃ f β) : Cardinal.{u} → Cardinal.{v} :=
Quotient.map f fun α β ⟨e⟩ => ⟨hf α β e⟩
