English
Let α and β be types with α = β. There exists a canonical isomorphism α ≃ β obtained by transporting along the equality h : α = β; the forward map is cast h and the inverse is cast h.symm.
Русский
Пусть α и β — типы и α = β. Существует естественное изоморфизм α ≃ β, получаемый переносом по равенству h: α = β; переходной функцией выступает cast h, обратной — cast h.symm.
LaTeX
$$$\\text{If } \\alpha = \\beta \\text{ then } \\alpha \\cong \\beta \\text{ via the transport along } h.\\; \\exists e:\\alpha \\simeq \\beta\\text{ with }e = \\operatorname{cast}(h).$$$
Lean4
/-- Equivalence between equal types. -/
protected def cast {α β : Sort _} (h : α = β) : α ≃ β
where
toFun := cast h
invFun := cast h.symm
left_inv := by grind
right_inv := by grind
