%--------------------------------------------------------------%
%   Author: Dragan Stosic                                      %
%--------------------------------------------------------------%
relation_extension[T, U: TYPE+]: THEORY
 BEGIN

 le_T: VAR equivalence[T]

 le_U: VAR equivalence[U]

 m, n: VAR [T, U]

 f: VAR [T -> U]

 g: VAR [U -> T]
  
 R: VAR equivalence[[T, U]]

 p_r1: VAR [[[T,U] -> T]]

 p_r2: VAR [[[T,U] -> U]]

 proj_tuple_1: [[[T,U] -> T]] = LAMBDA (m:[T,U]): m`1

 proj_tuple_2: [[[T,U] -> U]] = LAMBDA (m:[T,U]): m`2

 extended_equiv_class(R)(m): set[[T,U]] = { n | R(m, n) }

 extended_equiv_classT(R, p_r1, m, n) : set[T] = 
   { (t : T) | t= p_r1(m) AND  extended_equiv_class(R)(n)(m) }
 
 extended_equiv_classU(R, p_r2, m, n) : set[U] = 
   { (u : U) | u= p_r2(m) AND  extended_equiv_class(R)(n)(m) }
 
% extended equivalence relation based on two equivalence 
% relations : le_T , le_U

 rel_extension(le_T, le_U) : set[[[T, U], [T, U]]] =
   { (m, n) | le_T(m`1, n`1) AND le_U(m`2, n`2) }

 rel_extension_is_equivalence: JUDGEMENT
 rel_extension(le_T, le_U) HAS_TYPE equivalence[[T, U]]
                                                
% class representative for the rel_extension equivalence relation

 repEC_ext(le_T, le_U, m): [[T, U]] = repEC(rel_extension(le_T, le_U))(m)
    
END relation_extension