Trace cyclicity on Hom classes

The accompanying paper's Lemma 3.5(a) on the category: the descended trace of a composition is independent of the order. Bilinear induction with fragTrace_comm at the singles.

theorem RS.HomSpace.traceMap_comp_comm {R : ℕ} (f : EdgeRankParameter R) {t u : ℕ} (p : HomSpace f.val (t + u)) (q : HomSpace f.val (u + t)) : (traceMap f.val t) (((comp f t u t) p) q) = (traceMap f.val u) (((comp f u t u) q) p)

The descended trace is cyclic.