FundamentalGroupoid.ext

theorem FundamentalGroupoid.ext : ∀ {X : Type u} (x y : FundamentalGroupoid X), x.as = y.as → x = y

The theorem `FundamentalGroupoid.ext` states that for any type `X`, given two elements `x` and `y` of the type `FundamentalGroupoid X`, if the `as` attribute of `x` is equal to the `as` attribute of `y`, then `x` is equal to `y`. Essentially, this theorem says that two fundamental groupoids are equal if and only if their `as` attributes are equal.

More concisely: In the type of fundamental groupoids of a type X, elements with equal `as` attributes are equal.