Documentation

The semi-direct product of monoids s and m, which is a monoid when m acts on s. Structurally, the semi-direct product is just a pair (s,m). However, the monoid instance is different. In particular, we have

(s1,m1) <> (s2,m2) = (s1 <> (m1 `act` s2), m1 <> m2)

We call the monoid m the quotient monoid and the monoid s the sub-monoid of the semi-direct product. The semi-direct product Semi s m is an extension of the monoid s with m being the quotient.

Tag an s value with an m value to create an element of the semi-direct product.

The injection map, i.e. give an s value a trivial tag.

Forget the monoidal tag. Of course, untag . inject = id, and untag (tag s m) = s.

Embed a "tag" value as a value of type Semi s m. Note that

inject s <> embed m = tag s m

and

embed m <> inject s = tag (act m s) m@

The semi-direct product gives a split extension of s by m. This allows us to embed m into the semi-direct product. This is the embedding map. The quotient and embed maps should satisfy the equation quotient . embed = id.

The quotient map, i.e. retrieve the monoidal tag value.