English
For any F, G, A and X, Y with a morphism f: X → Y and η: F → G, together with p in YonedaCollection F Y, the two YonedaCollection operations commute: YonedaCollection.map₂ G f (YonedaCollection.map₁ η p) = YonedaCollection.map₁ η (YonedaCollection.map₂ F f p).
Русский
Для любых F, G, A и любых X, Y с морфизмом f: X → Y и η: F → G, а также p ∈ YonedaCollection F Y, два отображения YonedaCollection взаимно приводят к одному результату: YonedaCollection.map₂ G f (YonedaCollection.map₁ η p) = YonedaCollection.map₁ η (YonedaCollection.map₂ F f p).
LaTeX
$$$$ YonedaCollection.map₂\ G\ f\ ( YonedaCollection.map₁\ \eta\ p) = YonedaCollection.map₁\ \eta\ ( YonedaCollection.map₂\ F\ f\ p) $$$$
Lean4
@[simp]
theorem map₁_map₂ {G : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v} (η : F ⟶ G) {Y : C} (f : X ⟶ Y)
(p : YonedaCollection F Y) :
YonedaCollection.map₂ G f (YonedaCollection.map₁ η p) = YonedaCollection.map₁ η (YonedaCollection.map₂ F f p) := by
ext; all_goals simp
