fact: Definition forget (O: Object) : setoids.Object := setoids.object O.
imports: MathClasses.interfaces.abstract_algebra MathClasses.theory.categories MathClasses.orders.maps MathClasses.interfaces.orders MathClasses.orders.orders MathClasses.interfaces.functors