English
Let X and X' be graded objects and φ: X → X'. The inverse right unitor is natural in X, i.e., composing φ with the inverse of the right unitor for X' equals first applying the inverse right unitor for X and then mapping φ (tensored with the identity).
Русский
Пусть X и X' — градуированные объекты и φ: X → X'. Обратный правый унитор естественным образом зависит от аргумента: композиция φ с обратным правым унитором для X' равна сначала применению обратного правого унитора к X и затем отображению φ (с тензором единицы).
LaTeX
$$$\phi \circ (\mathrm{mapBifunctorRightUnitor} \, F \, Y \, e \, p \, hp \, X')^{-1} = (\mathrm{mapBifunctorRightUnitor} \, F \, Y \, e \, p \; hp \; X)^{-1} \circ \mathrm{mapBifunctorMapMap} F p \phi (\mathrm{Id})$$$
Lean4
@[reassoc]
theorem mapBifunctorRightUnitor_inv_naturality :
φ ≫ (mapBifunctorRightUnitor F Y e p hp X').inv =
(mapBifunctorRightUnitor F Y e p hp X).inv ≫ mapBifunctorMapMap F p φ (𝟙 _) :=
by
ext j
dsimp
rw [mapBifunctorRightUnitor_inv_apply, mapBifunctorRightUnitor_inv_apply, assoc, assoc, ι_mapBifunctorMapMap]
dsimp
rw [Functor.map_id, id_comp, NatTrans.naturality_assoc]
erw [← NatTrans.naturality_assoc e.inv]
rfl
