English
In a Cartesian closed setting with exponentials, the coevaluation morphism and the precomposition maps satisfy a naturality relation with respect to a morphism f: B → A: the left-hand and right-hand sides coincide when precomposing and evaluating appropriately.
Русский
В замкнутом по лексикону категориальном контексте с экспоненциалами коэв/пред-отображения удовлетворяют натуральному соотношению при отношении f: B → A: левая и правая части совпадают при подходящей префиксации и вычислении.
LaTeX
$$$ (\\mathrm{exp.coev} A)_{X} \\circ (\\mathrm{pre} f)_{A \\otimes X} = (\\mathrm{exp.coev} B)_{X} \\circ (\\mathrm{exp} B).map (f \\otimes \\mathrm{id}_X). $$$
Lean4
theorem coev_app_comp_pre_app (f : B ⟶ A) [Exponentiable B] :
(exp.coev A).app X ≫ (pre f).app (A ⊗ X) = (exp.coev B).app X ≫ (exp B).map (f ⊗ₘ 𝟙 _) :=
by
rw [tensorHom_id]
exact unit_conjugateEquiv _ _ ((tensoringLeft _).map f) X
