Setoids

Setoids are algebraic structures characterised by a domain and an equality relation.

 ** Module lib_setoid Imports parameters
 $Setoid : Type(Setoid)
 $make_Setoid : {dom:Type}(dom->dom->Prop)->Setoid
 $Setoid_elim :
    {C_Setoid:Setoid->TYPE}
    ({dom:Type}{eq1:dom->dom->Prop}C_Setoid (make_Setoid dom eq1))->
    {z:Setoid}C_Setoid z
[[C_Setoid:Setoid->TYPE]
 [f_make_Setoid:{dom:Type}{eq1:dom->dom->Prop}
  C_Setoid (make_Setoid dom eq1)][dom:Type][eq1:dom->dom->Prop]
    Setoid_elim C_Setoid f_make_Setoid (make_Setoid dom eq1)  ==>
    f_make_Setoid dom eq1]

  dom = ... : Setoid->Type
  eq1 = ... : {z:Setoid}(dom z)->(dom z)->Prop
  Setoid_eq = ... : {S|Setoid}(dom S)->(dom S)->Prop