Reduction of words in groupoid:

Stream: new members

[Rémi Bottinelli]

Hey,
I'm trying to prove that any element of the universal groupoid for a map is uniquely represented by a reduced word here.
I tried more or less following the structure in free_group.lean, but I feel like I'm working against the type system: Now words are indexed by their endpoints, and most inductions become quite messy or don't work at all.

In short:
If V is a groupoid and σ : V -> V' a map, we first define a quiver structure on V' by pushing that of Valong σ, take the path category on this structure, and quotient by the following relation:

inductive red.atomic_step : hom_rel (paths (quiver.push σ))
| comp (X Y Z : V) (f : X ⟶ Y) (g : Y ⟶ Z) :
    red.atomic_step
      ((σ † f) ≫ (σ † g))
      (σ † (f ≫ g))
| id (X : V) :
    red.atomic_step
      (σ † (𝟙 X))
      (𝟙 $ σ X)

where σ † f is the path in V' obtained by pushing the arrow f of V.
This works fine for defining the quotient and proving "abstract" things about this universal groupoid, but when it comes to the "messy" part of proving uniqueness of reduced words, it gets very painful and I get stuck at every step.
I'm wondering if I'm doing something wrong and/or there might be a better approach to this thing ?
Thanks!