Refactor extensionality of `Torsor-Abstract-Group`

[fredrik-bakke]

          The following probably doesn't type-check, but it will ge closer to what it should be (instead of an explicit pair of a function and a proof that it is an equivalence):

    ( inv-equiv (extensionality-Torsor-Abstract-Group G X))) ∘e

Originally posted by @EgbertRijke in #897 (comment)

Note that extensionality-Torsor-Abstract-Group is already defined