next up previous contents
Next: The Empty Type Up: Providing logic and equality Previous: Altenkirch-Streicher Elimination Rule


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

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

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

Fri May 24 19:01:27 BST 1996