English
The toList of the composite path equals the concatenation of the toLists: toList(p ∘ q) = toList(q) ++ toList(p).
Русский
ToList композиции пути равен конкатенации toList: toList(p ∘ q) = toList(q) ++ toList(p).
LaTeX
$$$\\forall p:\\, \\mathrm{Path}(a,b)\\;\\forall q:\\, \\mathrm{Path}(b,c),\\; \\mathrm{toList}(p\\circ q) = \\mathrm{toList}(q) \\;\\mathbin{++} \\mathrm{toList}(p).$$$
Lean4
/-- `Quiver.Path.toList` is a contravariant functor. The inversion comes from `Quiver.Path` and
`List` having different preferred directions for adding elements. -/
@[simp]
theorem toList_comp (p : Path a b) : ∀ {c} (q : Path b c), (p.comp q).toList = q.toList ++ p.toList
| _, nil => by simp
| _, @cons _ _ _ d _ q _ => by simp [toList_comp]
