English
For a functor f with a lawful behavior, there is a canonical way to transport an equivalence h: α ≃ β to an equivalence f α ≃ f β by applying f to both sides.
Русский
У функторa f с удовлетворяющим условиям поведением есть канонический способ перенести эквивалентность h: α ≃ β на эквивалентность f α ≃ f β путём применения f к обоим элементам.
LaTeX
$$$\\text{mapEquiv} : (\\alpha \\simeq \\beta) \\to (f \\alpha \\simeq f \\beta),\\; \\text{toFun} = \\text{map } h,\\; \\text{invFun} = \\text{map } h^{-1}$$$
Lean4
/-- Apply a functor to an `Equiv`. -/
def mapEquiv (h : α ≃ β) : f α ≃ f β where
toFun := map h
invFun := map h.symm
left_inv x := by simp [map_map]
right_inv x := by simp [map_map]
