$(a^{-1})^{-1} = a$ in a groupoid: proof review Exercise on groupoids article: Show that in a groupoid, $$
  (a^{-1})^{-1} = a \,.
$$
Proof: Every element must have an inverse, and likewise each element’s inverse must itself have an inverse (e.g., $a^{-1}$ must have an inverse $(a^{-1})^{-1})$, so $((a^{-1})^{-1} a^{-1}) a = a$, hence $(a^{-1})^{-1} ((a^{-1}) a) = a$ and thus $(a^{-1})^{-1} = a$.
Is my proof correct?
 A: The blog post in question defines things in the following way:

A groupoid is a set with a partially defined multiplication such that

*

*$a(bc) = (ab)c$, that is, whenever one side is defined so if the other and they are equal; additionally, when both $ab$ and $bc$ and are defined, so is $a(bc)$.

*every element $a$ has an inverse $a^{-1}$ such that both $a a^{-1}$ and $a^{-1} a$ are defined, [and] these products behave as identities “as much as possible”, namely, whenever $ab$ is defined, $a^{-1} a b = b$ and $a b b^{-1} = a$.


You start by (correctly) observing that $(a^{-1})^{-1} a^{-1} a = a$.
But I don’t see how to conclude from this single equation that $(a^{-1})^{-1} = a$.
I was originally not sure if the statement was even true, so I checked it in (too) much detail below.
However, we can also give a short argument:
abbreviating $a^{-1}$ and $(a^{-1})^{-1}$ as $a'$ and $a''$ respectively, we have
$$
  a
  = a'' a' a
  = a'' a' (a a' a'')
  = a'' (a' a a') a''
  = a'' a' a''
  = a'' \,.
$$

The long and tedious argumentation goes as follows:
The element $(a^{-1})^{-1}$ is defined via certain conditions.
We show that $(a^{-1})^{-1} = a$ by showing that the element $a$ satisfies these conditions.
More precisely, the element $(a^{-1})^{-1}$ is uniquely determined by the following four conditions:

*

*$a^{-1} (a^{-1})^{-1}$ is defined.


*$(a^{-1})^{-1} a^{-1}$ is defined.


*whenever $a^{-1} b$ is defined, $(a^{-1})^{-1} a^{-1} b = b$.


*whenever $b a^{-1}$ is defined, $b a^{-1} (a^{-1})^{-1} = b$.
We hence need to check that the element $a$ satisfies all of these conditions, when $(a^{-1})^{-1}$ is replaced by $a$.
More explicitly, we need to check the following four conditions:

*

*$a^{-1} a$ is defined.


*$a a^{-1}$ is defined.


*whenever $a^{-1} b$ is defined, $aa^{-1} b = b$,


*whenever $b a^{-1}$ is defined, $b a^{-1} a = b$.
To show these four conditions we are allowed to use all of the following:

*

*A. $x(yz)$ is defined if and only if $(xy)z$ is defined, and then both sides are equal (for arbitrary $x, y, z$).

Instead of $x(yz)$ or $(xy)z$, we then use the simplified notation $xyz$.
We will also use larger versions of associativity without further proof.

*

*B. If $xy$ and $yz$ are defined, then $xyz$ is defined (for arbitrary $x, y, z$).


*C. $x x^{-1}$ is defined (for arbitrary $x$).


*D. $x^{-1} x$ is defined (for arbitrary $x$).


*E. Whenever $xy$ is defined, $x^{-1} x y = y$ (for arbitrary $x, y$).


*F. Whenever $yx$ is defined, $y x x^{-1} = y$ (for arbitrary $x, y$).
This is enough to show 1, 2, 3 and 4.

*

*The first condition follows from D with $x = a$.


*The second condition follows from C with $x = a$.


*Suppose that $a^{-1} b$ is defined.
Since $a a^{-1}$ is defined by 2, it follows that $a a^{-1} b$ is defined.
We need to show that this element equals $b$.
We know that $a^{-1} a$ is defined by 1, it follows that $a^{-1} a a^{-1} b$ is defined.
It follows from E (with $x = a$ and $y = a^{-1} b$) that $a^{-1} a a^{-1} b = a^{-1} b$.
It follows from D that $(a^{-1})^{-1} a^{-1}$ is defined, whence we can extend the equality $a^{-1} a a^{-1} b = a^{-1} b$ to the equality
$$
  (a^{-1})^{-1} a^{-1} a a^{-1} b = (a^{-1})^{-1} a^{-1} b \,.
$$
But we know from E (with $x = a^{-1}$ and $y = a a^{-1} b$) that the left-hand site of this equation equals $a a^{-1} b$, and we also know from E (with $x = a^{-1}$ and $y = b$) that the right-hand side equals $b$.
Therefore, $a a^{-1} b = b$, as desired.


*Suppose now that $b a^{-1}$ is defined.
We know from 1 that $a^{-1} a$ is defined, so it follows that $b a^{-1} a$ is defined.
We need to show that this element equals $b$.
We know that $a a^{-1}$ is defined by 2, so it follows that $b a^{-1} a a^{-1}$ is defined.
We know from F (with $y = b a^{-1}$ and $x = a$) that $b a^{-1} a a^{-1} = b a^{-1}$.
We know from C that $a^{-1} (a^{-1})^{-1}$ is defined, whence we can extend the equality $b a^{-1} a a^{-1} = b a^{-1}$ to the equality
$$
  b a^{-1} a a^{-1} (a^{-1})^{-1} = b a^{-1} (a^{-1})^{-1} \,.
$$
We know from F (with $y = b a^{-1} a$ and $x = a^{-1}$) that the left-hand side of this equation equals $b a^{-1} a$, and we also know from F (with $y = b$ and $x = a^{-1}$ that the right-side equals $b$.
Therefore, $b a^{-1} a = b$, as desired.
In short form, the above two argumentations read as
$$
  a a^{-1} b
  = (a^{-1})^{-1} a^{-1} a a^{-1} b
  = (a^{-1})^{-1} a^{-1} b
  = b
$$
and
$$
  b a^{-1} a
  = b a^{-1} a a^{-1} (a^{-1})^{-1}
  = b a^{-1} (a^{-1})^{-1}
  = b \,.
$$
