1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "properties/relations1.ma".
16 include "sets/setoids.ma".
18 nrecord setoid1: Type[2] ≝
20 eq1: equivalence_relation1 carr1
23 ndefinition setoid1_of_setoid: setoid → setoid1.
26 | napply (mk_equivalence_relation1 s)
33 (*ncoercion setoid1_of_setoid : ∀s:setoid. setoid1 ≝ setoid1_of_setoid
34 on _s: setoid to setoid1.*)
35 (*prefer coercion Type_OF_setoid.*)
37 interpretation "setoid1 eq" 'eq t x y = (eq_rel1 ? (eq1 t) x y).
38 interpretation "setoid eq" 'eq t x y = (eq_rel ? (eq t) x y).
40 notation > "hvbox(a break =_12 b)" non associative with precedence 45
41 for @{ eq_rel2 (carr2 (setoid2_of_setoid1 ?)) (eq2 (setoid2_of_setoid1 ?)) $a $b }.
42 notation > "hvbox(a break =_0 b)" non associative with precedence 45
43 for @{ eq_rel ? (eq ?) $a $b }.
44 notation > "hvbox(a break =_1 b)" non associative with precedence 45
45 for @{ eq_rel1 ? (eq1 ?) $a $b }.
47 interpretation "setoid1 symmetry" 'invert r = (sym1 ???? r).
48 interpretation "setoid symmetry" 'invert r = (sym ???? r).
49 notation ".= r" with precedence 50 for @{'trans $r}.
50 interpretation "trans1" 'trans r = (trans1 ????? r).
51 interpretation "trans" 'trans r = (trans ????? r).
53 nrecord unary_morphism1 (A,B: setoid1) : Type[1] ≝
55 prop11: ∀a,a'. eq1 ? a a' → eq1 ? (fun11 a) (fun11 a')
58 nrecord binary_morphism1 (A,B,C:setoid1) : Type[1] ≝
60 prop21: ∀a,a',b,b'. eq1 ? a a' → eq1 ? b b' → eq1 ? (fun21 a b) (fun21 a' b')
63 interpretation "prop11" 'prop1 c = (prop11 ????? c).
64 interpretation "prop21" 'prop2 l r = (prop21 ???????? l r).
65 interpretation "refl1" 'refl = (refl1 ???).