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). *)