How do I find an inverse of any element in any group?

Question

I'm working on Agda, which is based on intuitionistic type theory. I defined groups in Agda with normal laws of groups, which (of course not only) says that there is an inverse element of every element of every group.

The question is, as I've defined, there exists such inverse, but how do I actually get that inverse? i.e. write a function $ inverse : G \to G $ where $ G $ is a group. Is it even possible? For example, given the group $ (\mathbb{Z}, +, 0) $, I want $ inverse(2) = -2 $.

Alternatively, can I prove $ inverse(inverse(a)) = a $ (or its equivalence) without such concrete $ inverse $ function?

Here is the Agda code:

data Sigma {l} (A : Set l) (B : A -> Set l) : Set l where
  _**_ : (a : A) -> B a -> Sigma A B

record Group {l} (G : Set l) (_op_ : G -> G -> G) (e : G) : Set l where
  field
    assoc : {a b c : G} -> (a op b) op c == a op (b op c)
    id : {a : G} -> e op a == a
    inv : {a : G} -> Sigma G (\a^-1 -> a^-1 op a == e)

_^-1 : forall {l} {G : Set l} {op : G -> G -> G} {e : G} {{inst : Group G op e}} -> G -> G
_^-1 {{inst}} a = ?

Answer 1

Alternatively, can I prove $(a^{−1})^{−1}=a$ (or its equivalence) without such concrete inverse function?

Sure. The axioms of inversion, along with the axiom of identity allows you to prove the inverse of an element is unique.

If $ab=e$ for some element $b$, then $b=eb=a^{-1}ab=a^{-1}e=a^{-1}$.

Then since $a^{-1}(a^{−1})^{−1}=(a^{−1})^{−1}a^{-1}=e$, and also $a^{-1}a=aa^{-1}=e$, $a$ and $(a^{-1})^{-1}$ must be the same thing.