Given a set of relations, rels, over a type α, presented_group constructs the group with generators α and relations rels as a quotient of free_group α.

of x is the canonical map from α to a presented group with generators α. The term x is mapped to the equivalence class of the image of x in free_group α.

The extension of a map f : α → β that satisfies the given relations to a group homomorphism from presented_group rels → β.