MATH.1:4.2 - Form finite paths
A path of length n>0 is a list [a1,…,an] with t(ai)=s(a(i+1)) for every adjacent pair. Its source is s(a1) and its target is t(an).
At each object x, add an empty path id_x. It starts and ends at x and contains no generator. Keeping its object matters: the empty path at one object cannot serve as the identity at another.
Initially, two nonempty paths are equal when their lists contain the same generators in the same order. The empty paths are equal only at the same object. This choice retains the sequence used to construct the path. A later identification can deliberately forget part of it, using MATH.2.
Construct only the paths needed for the immediate question, or describe a family by its formation rule. Cycles make infinitely many paths possible, but each path remains finite.