English
Left associator for Holor: there is a canonical transport from Holor α (ds1 ++ (ds2 ++ ds3)) to Holor α (ds1 ++ ds2 ++ ds3) given by casting along the inverse associativity.
Русский
Левый ассоциатор для Holor: существует канонический перенос из Holor α (ds1 ++ (ds2 ++ ds3)) в Holor α (ds1 ++ ds2 ++ ds3) через cast с инверсией ассоциативности.
LaTeX
$$$\operatorname{assocLeft} : 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).symm)$$
Lean4
/-- Left associator for `Holor` -/
def assocLeft : Holor α (ds₁ ++ (ds₂ ++ ds₃)) → Holor α (ds₁ ++ ds₂ ++ ds₃) :=
cast (congr_arg (Holor α) (append_assoc ds₁ ds₂ ds₃).symm)
