English
The addition with the right zero interacts with shift by zero via an isomorphism between shiftFunctorAdd and a whiskered shiftFunctor.
Русский
Сложение с нулём справа взаимодействует со сдвигом через изоморфизм между shiftFunctorAdd и whiskered shiftFunctor.
LaTeX
$$$\\text{shiftFunctorAdd'_add_zero} = \\mathrm{rightUnitor} \\;\\text{trans}\\; (\\mathrm{shiftFunctor} \\; a) \\circ \\mathrm{isoWhiskerLeft}(\\mathrm{shiftFunctor}, \\mathrm{shiftFunctorZero})$$$
Lean4
theorem shiftFunctorAdd'_add_zero (a : A) :
shiftFunctorAdd' C a 0 a (add_zero a) =
(rightUnitor _).symm ≪≫ isoWhiskerLeft (shiftFunctor C a) (shiftFunctorZero C A).symm :=
by
ext
dsimp [shiftFunctorAdd', shiftFunctorZero, shiftFunctor]
simp only [eqToHom_app, ε_app_obj, Discrete.addMonoidal_rightUnitor, eqToIso.inv, eqToHom_map, Category.id_comp]
rfl
