English
A version of arrowCongr for Type with refls: arrowCongr' (Equiv.refl α) (Equiv.refl β) = Equiv.refl (α → β).
Русский
Версия arrowCongr' для типа с тождествами: arrowCongr' (refl α) (refl β) = refl (α → β).
LaTeX
$$$\mathrm{arrowCongr'}(\mathrm{refl}\, \alpha)(\mathrm{refl}\, \beta) = \mathrm{refl}\,(\alpha \to \beta)$$$
Lean4
/-- A version of `Equiv.arrowCongr` in `Type`, rather than `Sort`.
The `equiv_rw` tactic is not able to use the default `Sort` level `Equiv.arrowCongr`,
because Lean's universe rules will not unify `?l_1` with `imax (1 ?m_1)`.
-/
@[simps! (attr := grind =) apply]
def arrowCongr' {α₁ β₁ α₂ β₂ : Type*} (hα : α₁ ≃ α₂) (hβ : β₁ ≃ β₂) : (α₁ → β₁) ≃ (α₂ → β₂) :=
Equiv.arrowCongr hα hβ
