setoid http://www.openmath.org/cd/setoid.ocd 2003-04-01 experimental 1999-06-01 1 1 The definition of a setoid as a set with an equivalence relations defined on its elements. Initial version: O. Caprotti Setoid The contructor for the type of set with an equivalence relation on it. Is defined as Lambda {Carrier:> symtype; Eq: (relation Carrier)}. SigmaType{ Carrier:> symtype; Eq: (relation Carrier); (equivalence Carrier Eq) } make_Setoid The contructor for the tuples consisting of a set, an equivalence relation on the set, and a proof that the relation is actually an equivalence relation. Is defined as Lambda {Carrier:> symtype; Eq: (relation Carrier) proof: (equivalence Carrier Eq)}. Tuple (Carrier, Eq, proof)