]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/nlibrary/sets/setoids.ma
...
[helm.git] / helm / software / matita / nlibrary / sets / setoids.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "logic/connectives.ma".
16 include "properties/relations.ma".
17
18 (*
19 notation "hvbox(a break = \sub \ID b)" non associative with precedence 45
20 for @{ 'eqID $a $b }.
21
22 notation > "hvbox(a break =_\ID b)" non associative with precedence 45
23 for @{ cic:/matita/logic/equality/eq.ind#xpointer(1/1) ? $a $b }.
24
25 interpretation "ID eq" 'eqID x y = (cic:/matita/logic/equality/eq.ind#xpointer(1/1) ? x y).
26 *)
27
28 nrecord setoid : Type[1] ≝
29  { carr:> Type[0];
30    eq: equivalence_relation carr
31  }.
32
33 interpretation "setoid eq" 'eq t x y = (eq_rel ? (eq t) x y).
34
35 notation > "hvbox(a break =_0 b)" non associative with precedence 45
36 for @{ eq_rel ? (eq ?) $a $b }.
37
38 interpretation "setoid symmetry" 'invert r = (sym ???? r).
39 notation ".= r" with precedence 50 for @{'trans $r}.
40 interpretation "trans" 'trans r = (trans ????? r).
41
42 nrecord unary_morphism (A,B: setoid) : Type[0] ≝
43  { fun1:1> A → B;
44    prop1: ∀a,a'. eq ? a a' → eq ? (fun1 a) (fun1 a')
45  }.
46
47 nrecord binary_morphism (A,B,C:setoid) : Type[0] ≝
48  { fun2:2> A → B → C;
49    prop2: ∀a,a',b,b'. eq ? a a' → eq ? b b' → eq ? (fun2 a b) (fun2 a' b')
50  }.
51
52 notation "† c" with precedence 90 for @{'prop1 $c }.
53 notation "l ‡ r" with precedence 90 for @{'prop2 $l $r }.
54 notation "#" with precedence 90 for @{'refl}.
55 interpretation "prop1" 'prop1 c  = (prop1 ????? c).
56 interpretation "prop2" 'prop2 l r = (prop2 ???????? l r).
57 interpretation "refl" 'refl = (refl ???).