English
For a morphism φ: X → X' between graded objects, the map mapBifunctorMapMap F p φ (Id) intertwines with the forward right unitor, giving a commutative relation with the right unitor on X and X'.
Русский
Для морфинa φ: X → X' между градуированными объектами отображение mapBifunctorMapMap F p φ (Id) взаимно согласуется с правым унитором: образует commute-диаграмму с правым унитором на X и X'.
LaTeX
$$$$ (\mathrm{mapBifunctorMapMap}\, F\, p\, φ\, (\mathrm{Id})) \, ; \, (\mathrm{mapBifunctorRightUnitor}\, F\, Y\, e\, p\, hp\, X').\mathrm{hom} = (\mathrm{mapBifunctorRightUnitor}\, F\, Y\, e\, p\, hp\, X).\mathrm{hom} \, ; \, φ $$$$
Lean4
@[reassoc]
theorem mapBifunctorRightUnitor_naturality :
mapBifunctorMapMap F p φ (𝟙 _) ≫ (mapBifunctorRightUnitor F Y e p hp X').hom =
(mapBifunctorRightUnitor F Y e p hp X).hom ≫ φ :=
by
rw [← cancel_mono (mapBifunctorRightUnitor F Y e p hp X').inv, assoc, assoc, Iso.hom_inv_id, comp_id,
mapBifunctorRightUnitor_inv_naturality, Iso.hom_inv_id_assoc]
