English
Let e1: A1 ≃ A2 and e2: B1 ≃ B2. The inverse of the induced map arrowCongr' e1 e2 equals the induced map arrowCongr' e1^{-1} e2^{-1}. In other words, transporting functions along e1 and e2 and then inverting is the same as transporting along the inverses.
Русский
Пусть e1: A1 ≃ A2 и e2: B1 ≃ B2. Обратное отображение, индуцированное стрелочной конгруэнтностью arrowCongr' e1 e2, равно arrowCongr' e1^{-1} e2^{-1}. Иными словами, перенос функций по e1 и e2 с последующим взятием обратного равен переносу по обратным отображениям.
LaTeX
$$$ (\operatorname{arrowCongr}'\, e_1\, e_2)^{-1} = \operatorname{arrowCongr}'\, e_1^{-1}\, e_2^{-1} $$$
Lean4
@[simp, grind =]
theorem arrowCongr'_symm {α₁ α₂ β₁ β₂ : Type*} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) :
(arrowCongr' e₁ e₂).symm = arrowCongr' e₁.symm e₂.symm :=
rfl
