English
Right associator for Holor: there is a canonical transport from Holor α (ds1 ++ ds2 ++ ds3) to Holor α (ds1 ++ (ds2 ++ ds3)) given by casting along the associativity of concatenation.
Русский
Правый ассоциатор для Holor: существует канонический перенос из Holor α (ds1 ++ ds2 ++ ds3) в Holor α (ds1 ++ (ds2 ++ ds3)), задаваемый приведением вдоль ассоциативности конкатенации.
LaTeX
$$$\operatorname{assocRight} : Holor\, \alpha\, (ds_1 ++ ds_2 ++ ds_3) \to Holor\, \alpha\, (ds_1 ++ (ds_2 ++ ds_3)) \\ = \\ cast (congr_arg (Holor\, \alpha) (append_assoc ds_1 ds_2 ds_3))$$
Lean4
/-- Right associator for `Holor` -/
def assocRight : Holor α (ds₁ ++ ds₂ ++ ds₃) → Holor α (ds₁ ++ (ds₂ ++ ds₃)) :=
cast (congr_arg (Holor α) (append_assoc ds₁ ds₂ ds₃))
