English
Let F be a functor from C to D. For any objects X,Y in C and any equality p: X = Y, the canonical isomorphism between F(X) and F(Y) obtained from p coincides with the isomorphism obtained by transporting along F.obj, i.e. F.mapIso(eqToIso(p)) = eqToIso(congr_arg F.obj p).
Русский
Пусть F — функтор C ⟶ D. Пусть X, Y — объекты C и p: X = Y. Тогда каноническое изоморфизм между F(X) и F(Y), полученное из p, совпадает с изоморфизмом, полученным через применении F к p, то есть F.mapIso(eqToIso(p)) = eqToIso(congr_arg F.obj p).
LaTeX
$$$F.mapIso(\\mathrm{eqToIso}(p)) = \\mathrm{eqToIso}(\\mathrm{congrArg} F.obj\\, p)$$$
Lean4
/-- See the note on `eqToHom_map` regarding using this as a `simp` lemma.
-/
theorem eqToIso_map (F : C ⥤ D) {X Y : C} (p : X = Y) : F.mapIso (eqToIso p) = eqToIso (congr_arg F.obj p) := by ext;
cases p; simp
