fact: Definition fold `{MonUnit M} `{SgOp M}: free M → M := extend id.
imports: Coq.Lists.List MathClasses.interfaces.abstract_algebra MathClasses.theory.categories MathClasses.theory.forget_algebra MathClasses.theory.forget_variety MathClasses.theory.rings MathClasses.interfaces.universal_algebra MathClasses.interfaces.functors MathClasses.categories.setoids MathClasses.categories.varieties