English
If α ≃ β and γ ≃ δ, then there is a canonical equivalence (α ≃ γ) ≃ (β ≃ δ) sending e to (ab.symm.trans e).trans cd.
Русский
Если α ≃ β и γ ≃ δ, существует каноническое соответствие (α ≃ γ) ≃ (β ≃ δ), отправляющее e в (ab^{-1} ∘ e ∘ cd).
LaTeX
$$def equivCongr {δ : Sort*} (ab : α ≃ β) (cd : γ ≃ δ) : (α ≃ γ) ≃ (β ≃ δ)$$
Lean4
/-- If `α` is equivalent to `β` and `γ` is equivalent to `δ`, then the type of equivalences `α ≃ γ`
is equivalent to the type of equivalences `β ≃ δ`. -/
def equivCongr {δ : Sort*} (ab : α ≃ β) (cd : γ ≃ δ) : (α ≃ γ) ≃ (β ≃ δ)
where
toFun ac := (ab.symm.trans ac).trans cd
invFun bd := ab.trans <| bd.trans <| cd.symm
left_inv ac := by grind
right_inv ac := by grind
