English
For any morphism f: X → Y of simplicial sets and any level n, the action of the opposite functor on f at level n coincides with first applying f to the identified representative and then transporting back along the canonical X.op-identification.
Русский
Для любого морфизма f: X → Y между симпликальными множествами и любого уровня n действие функторa противоположности на f на уровне n совпадает с применением f к представляющему элементу в X и последующей обратной транспортировкой по каноническому соответствию X.op.
LaTeX
$$$(opFunctor.map f).app_n x = opObjEquiv.symm \\bigl( f.app_n (opObjEquiv x) \\bigr)$$$
Lean4
theorem opFunctor_map {X Y : SSet.{u}} (f : X ⟶ Y) {n : SimplexCategoryᵒᵖ} (x : X.op.obj n) :
(opFunctor.map f).app n x = opObjEquiv.symm (f.app _ (opObjEquiv x)) :=
rfl
