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 https://github.com/UniMath/agda-unimath/pull/897#discussion_r1380064315

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