semigroup http://www.openmath.org/cd/semigroup.ocd 2003-04-01 experimental 1999-09-29 1 1 The definition of a semigroup as setoid with a binary operation. Initial version: O. Caprotti associative The type of associative binary operation. Is defined as Lambda {sg_Carrier:> Setoid; sg_op: mapsto(sg_Carrier sg_Carrier sg_Carrier)}. PiType{ x,y,z: sg_Carrier }. eq(sg_op(x, sg_op(y,z)), sg_op( sg_op(x,y),z)) Semigroup The contructor for the type of semigroups as a Setoid with a binary operation. Is defined as Lambda {sg_Carrier:> Setoid; sg_op: mapsto(sg_Carrier sg_Carrier sg_Carrier)}. SigmaType{ sg_Carrier:> Setoid; sg_op: mapsto(sg_Carrier sg_Carrier sg_Carrier); (associative sg_Carrier sg_op) } make_Semigroup The contructor for the tuples consisting of a setoid, and an associative binary operation. Is defined as Lambda {sg_Carrier:> Setoid; sg_op: mapsto(sg_Carrier sg_Carrier sg_Carrier); proof: (associative sg_Carrier sg_op)}. Tuple (Setoid, sg_op, proof)