Naming of foldTrans/concatenate for paths

Stream: mathlib4

[Sebastian Kumar]

I have the following function that, given a sequence of paths with compatible endpoints, concatenates them together into one path (for use in proving that the sphere is simply connected). I called it Path.foldTrans based on the implementation, but I am not sure if Path.concatenate or something like that would be a better name. I wanted to get some feedback here before I made a pull request to mathlib. Thoughts? Also, if I do use foldTrans, would I name theorems like theorem_about_fold_trans or theorem_about_foldTrans?

import Mathlib
import Batteries.Data.Fin.Fold

open Fin

universe u

variable {X : Type u} [TopologicalSpace X] {n : ℕ}

namespace Path

/-- Folds `Path.trans` across a sequence of paths with compatatible endpoints. -/
noncomputable def foldTrans (p : Fin (n + 1) → X)
    (F : ∀ k : Fin n, Path (p k.castSucc) (p k.succ)) : Path (p 0) (p (last n)) :=
  dfoldl n (fun i => Path (p 0) (p i)) (fun i ih => ih.trans (F i)) (refl (p 0))

end Path