English
The shift addition with zero on the left is equal to left-unitor composed with whisker of shiftFunctorZero, illustrating a canonical coherence.
Русский
Композиция shiftFunctorAdd' при нулевом левом аргументе равна канонической коэрцерции через leftUnitor и whisker.
LaTeX
$$$\\text{shiftFunctorAdd'_zero_add} = (\\text{leftUnitor}()).symm \\;\\text{trans}\\; \\mathrm{isoWhiskerRight}(\\text{shiftFunctorZero}, \\text{shiftFunctor})$$$
Lean4
theorem shiftFunctorAdd'_zero_add (a : A) :
shiftFunctorAdd' C 0 a a (zero_add a) =
(leftUnitor _).symm ≪≫ isoWhiskerRight (shiftFunctorZero C A).symm (shiftFunctor C a) :=
by
ext X
dsimp [shiftFunctorAdd', shiftFunctorZero, shiftFunctor]
simp only [eqToHom_app, obj_ε_app, Discrete.addMonoidal_leftUnitor, eqToIso.inv, eqToHom_map, Category.id_comp]
rfl
