The presentation of the link-homotopy classes over a closed surface (Theorem 3.9)

import Mathlib
import Definitions.Def_HGL_alg
import Definitions.Def_HGL_tor

namespace HGL

/-!  The goal (Theorem 3.9): for a closed orientable surface M of genus g,
the group of link-homotopy classes of generalized string links over M
admits the presentation with the generators a_(1,1), ..., a_(1,2g) and
sigma_1, ..., sigma_(n-1) and the relations LH - the commutator of the
t-word with its conjugates - together with the relations R1 through R6 of
the Gonzalez-Meneses presentation. The universal property: any group with
families satisfying these relations receives a unique homomorphism from the
class group mapping the standard generators to the families. -/
theorem presentation_universal {n g : ℕ} {B S Cl : Type*} [Group B] [Monoid S] [Group Cl]
    (W : LinkHomotopyWorld n g B S Cl) :
    ∀ (G : Type) [Group G] (sigma : Fin (n - 1) → G) (a : Fin (2 * g) → G),
      SatisfiesPresentation W.hn sigma a →
      ∃! f : Cl →* G, (∀ i : Fin (n - 1), f (W.gen_sigma i) = sigma i) ∧
        (∀ r : Fin (2 * g), f (W.gen_a r) = a r) := by sorry

end HGL