Problem #3 Template

A common elementary exercise in abstract algebra is to show that a finite monoid with the cancellation property is in fact a group. Perhaps less known is that one can weaken the assumption of a monoid to a semigroup, provided of course that the semigroup is non-empty.

In constructive mathematics, you have to be careful about what precisely you mean by ‘finite’. For the purposes of this problem, the most natural notion of finiteness is that of Dedekind-finiteness. We will say that a set X is Dedekind-finite if every injection X -> X is also a surjection.

Problem: Given a Dedekind-finite semigroup which is inhabited and satisfies the cancellation property, construct an identity and inverse operation, and prove that they satisfy their respective group laws.