English
A natural transformation α : P ⟶ Q between pairs P, Q in the product category acts on x ∈ (coyonedaEvaluation C).obj P by mapping to the down-projection of the result; this equals α.2.app(Q.1) applied to P.2.map(α.1) on x.down.
Русский
Пусть α : P ⟶ Q — натуральное преобразование между парами P, Q в произведенной категории; тогда для x ∈ (coyonedaEvaluation C).obj P картина down-коэффициента после отображения равна применению α.2.app(Q.1) к (P.2.map(α.1) на x.down).
LaTeX
$$$$ ((\mathrm{coyonedaEvaluation}(C)).map \alpha x)^{\downarrow} = \alpha_2.\mathrm{app}_{Q_1}(P_2.\mathrm{map}(\alpha_1)(x^{\downarrow})) $$$$
Lean4
@[simp]
theorem coyonedaEvaluation_map_down (P Q : C × (C ⥤ Type v₁)) (α : P ⟶ Q) (x : (coyonedaEvaluation C).obj P) :
((coyonedaEvaluation C).map α x).down = α.2.app Q.1 (P.2.map α.1 x.down) :=
rfl
