Monoid condition for decidable exponentials

ID: monoid-condition-for-decidable-exponentials

If each admits with , then is decidable whenever the left M-set is. For equivariant , equality of all values at implies equality at : apply and use , then cancel the injective action of on . Equality after the exponential action of then gives equal traces by cancelling its action on .

New to topics? Read the docs here!