include "hints_declaration.ma".
include "basics/types.ma".
include "basics/relations.ma".

record Setoid : Type[1] ≝ {
  std_supp :> Type[0] ;
  std_eq : relation std_supp;
  std_refl : reflexive ? std_eq;
  std_trans : transitive ? std_eq;
  std_symm : symmetric ? std_eq
}.

definition as_std : Type[0] → Setoid ≝
  λT.mk_Setoid T (eq T) (refl T) (trans_eq T) (sym_eq T).

(* coercion setoid_from_set nocomposites:
  ∀t : Type[0].Setoid ≝ set_to_setoid on _t : Type[0] to Setoid.*)

interpretation "setoid equality" 'std_eq x y = (std_eq ? x y).

notation "x ≅ y" with precedence 45 for @{'std_eq $x $y}.

definition std_prod ≝ λX,Y : Setoid.mk_Setoid (X×Y)
  (λp,q. 'pi1 p ≅ 'pi1 q ∧ 'pi2 p ≅ 'pi2 q) ???./2/
[(* transitivity *)
  *#p1#p2*#q1#q2*#r1#r2*#H1#H2*#H3#H4 %/2/
|(* symmetry *)
  *#p1#p2*#q1#q2*#H1#H2%/2/
]qed.

(*
interpretation "Setoid Product" 'product X Y = (std_pair X Y).
*)

definition std_union ≝ λX,Y : Setoid.mk_Setoid (X+Y)
  (λp,q. match p with
    [inl x ⇒ match q with
      [ inl y ⇒ x ≅ y
      | _ ⇒ False
      ]
    |inr x ⇒ match q with
      [ inr y ⇒ x ≅ y
      | _ ⇒ False
      ]
    ]) ???.
[(* reflexivity *)
  *#x normalize //
|
  (* transitivity *)
  *#x normalize *#y normalize *#z normalize /2/ #F elim F
|(* symmetry *)
  *#x normalize *#y normalize /2/
]qed.

(* interpretation "setoid union" 'plus X Y = (std_union X Y). *)