(def-language relational-language
    (base-types uu)
    (constants 
      (equiv "[uu,uu,prop]"0)))

(def-theory relational-theory 
    (language relational-language)
    (component-theories h-o-real-arithmetic)
    (axioms
      (equiv-transitivity
        "forall(a,b,c:uu, a equiv b and b equiv c implies a equiv c)")
      (equiv-reflexivity
        "forall(a:uu, a equiv a)")
      (equiv-symmetry
        "forall(a,b:uu, a equiv b implies b equiv a)")))

(def-constant equiv%class 
    "lambda(x:uu, indic{y:uu, x equiv y})"
    (theory relational-theory))
    

(def-constant equiv%class_q 
    "lambda(a:sets[uu], forsome(y:uu, a=equiv%class(y)))"
    (theory relational-theory))

(def-theorem ()
    "forsome(a:sets[uu], equiv%class_q(a))"
    (theory relational-theory)
    (proof
      (
        (instantiate-existential ("with(x:uu,equiv%class(x))"))
        unfold-defined-constants
        unfold-defined-constants
        (instantiate-existential ("x"))
        unfold-defined-constants
        )))

(def-atomic-sort uu_q 
    "equiv%class_q"
    (theory relational-theory))
		          

(def-theory-ensemble relational-theory)

(def-theory-ensemble-multiple relational-theory 2)

(def-theory-ensemble-overloadings metric-spaces (1))

(def-overloading equiv
    (relational-theory equiv) 
    (relational-theory-2-tuples equiv_0)
    (relational-theory-2-tuples equiv_1))

(def-constant equiv%on%classes%unary 
    "lambda(f:[uu_0,uu_1], forall(a,b:uu_0, a equiv b implies f(a) equiv f(b)))"
    (theory relational-theory-2-tuples))