English
A higher coherence expresses that two different regroupings of three shifts yield the same natural transformation up to isomorphism.
Русский
Высшая коherence показывает, что две различные перекрестки трёх сдвигов эквивалентны через естественные преобразования на уровне изоморфий.
LaTeX
$$$\\text{ShiftAdd}'(a_1,a_2) \\circ \\text{ShiftAdd}'(a_2,a_3) = \\text{ShiftAdd}'(a_1,a_2,a_3)$$$
Lean4
theorem shiftFunctorAdd_assoc (a₁ a₂ a₃ : A) :
shiftFunctorAdd C (a₁ + a₂) a₃ ≪≫ isoWhiskerRight (shiftFunctorAdd C a₁ a₂) _ ≪≫ associator _ _ _ =
shiftFunctorAdd' C a₁ (a₂ + a₃) _ (add_assoc a₁ a₂ a₃).symm ≪≫ isoWhiskerLeft _ (shiftFunctorAdd C a₂ a₃) :=
by
ext X
simpa [shiftFunctorAdd'_eq_shiftFunctorAdd] using
NatTrans.congr_app (congr_arg Iso.hom (shiftFunctorAdd'_assoc C a₁ a₂ a₃ _ _ _ rfl rfl rfl)) X
