∀ {X : Type u_1} [inst : TopologicalSpace X] {x₀ x₁ : X} (f g : Path x₀ x₁),
  FundamentalGroupoid.fromPath (Path.Homotopic.Quotient.mk f) =
      FundamentalGroupoid.fromPath (Path.Homotopic.Quotient.mk g) ↔
    f.Homotopic g