Relations are now closer to Sambin's ones. I.e. they range over Types

and not (sub)sets.

diff --git a/helm/software/matita/library/formal_topology/relations.ma b/helm/software/matita/library/formal_topology/relations.ma
index e67b2ce7c5ea8792fd4b715efb3befe79dcaa2c5..033788e928fb193b877330b806c89a8cf92281cc 100644 (file)
--- a/helm/software/matita/library/formal_topology/relations.ma
+++ b/helm/software/matita/library/formal_topology/relations.ma
@@ -14,61 +14,54 @@
 
 include "datatypes/subsets.ma".
 
-record ssigma (A:Type) (S: powerset A) : Type ≝
- { witness:> A;
-   proof:> witness ∈ S
- }.
-
-coercion ssigma.
-
-record binary_relation (A,B: Type) (U: Ω \sup A) (V: Ω \sup B) : Type ≝
- { satisfy:2> U → V → CProp }.
+record binary_relation (A,B: Type) : Type ≝
+ { satisfy:2> A → B → CProp }.
 
 notation < "hvbox (x \nbsp \natur term 90 r \nbsp y)"  with precedence 45 for @{'satisfy $r $x $y}.
 notation > "hvbox (x \natur term 90 r y)"  with precedence 45 for @{'satisfy $r $x $y}.
-interpretation "relation applied" 'satisfy r x y = (satisfy ____ r x y).
+interpretation "relation applied" 'satisfy r x y = (satisfy __ r x y).
 
 definition composition:
- ∀A,B,C.∀U1: Ω \sup A.∀U2: Ω \sup B.∀U3: Ω \sup C.
-  binary_relation ?? U1 U2 → binary_relation ?? U2 U3 →
-   binary_relation ?? U1 U3.
- intros (A B C U1 U2 U3 R12 R23);
+ ∀A,B,C.
+  binary_relation A B → binary_relation B C →
+   binary_relation A C.
+ intros (A B C R12 R23);
  constructor 1;
  intros (s1 s3);
  apply (∃s2. s1 ♮R12 s2 ∧ s2 ♮R23 s3);
 qed.
 
-interpretation "binary relation composition" 'compose x y = (composition ______ x y).
+interpretation "binary relation composition" 'compose x y = (composition ___ x y).
 
 definition equal_relations ≝
- λA,B,U,V.λr,r': binary_relation A B U V.
+ λA,B.λr,r': binary_relation A B.
   ∀x,y. r x y ↔ r' x y.
 
-interpretation "equal relation" 'eq x y = (equal_relations ____ x y).
+interpretation "equal relation" 'eq x y = (equal_relations __ x y).
 
-lemma refl_equal_relations: ∀A,B,U,V. reflexive ? (equal_relations A B U V).
- intros 5; intros 2; split; intro; assumption.
+lemma refl_equal_relations: ∀A,B. reflexive ? (equal_relations A B).
+ intros 3; intros 2; split; intro; assumption.
 qed.
 
-lemma sym_equal_relations: ∀A,B,U,V. symmetric ? (equal_relations A B U V).
- intros 7; intros 2; split; intro;
+lemma sym_equal_relations: ∀A,B. symmetric ? (equal_relations A B).
+ intros 5; intros 2; split; intro;
   [ apply (fi ?? (H ??)) | apply (if ?? (H ??))] assumption.
 qed.
 
-lemma trans_equal_relations: ∀A,B,U,V. transitive ? (equal_relations A B U V).
- intros 9; intros 2; split; intro;
+lemma trans_equal_relations: ∀A,B. transitive ? (equal_relations A B).
+ intros 7; intros 2; split; intro;
   [ apply (if ?? (H1 ??)) | apply (fi ?? (H ??)) ]
   [ apply (if ?? (H ??)) | apply (fi ?? (H1 ??)) ]
   assumption.
 qed.
 
 lemma associative_composition:
- ∀A,B,C,D.∀U1,U2,U3,U4.
-  ∀r1:binary_relation A B U1 U2.
-   ∀r2:binary_relation B C U2 U3.
-    ∀r3:binary_relation C D U3 U4.
+ ∀A,B,C,D.
+  ∀r1:binary_relation A B.
+   ∀r2:binary_relation B C.
+    ∀r3:binary_relation C D.
      (r1 ∘ r2) ∘ r3 = r1 ∘ (r2 ∘ r3).
- intros 13;
+ intros 9;
  split; intro;
  cases H; clear H; cases H1; clear H1;
  [cases H; clear H | cases H2; clear H2]
@@ -80,11 +73,11 @@ lemma associative_composition:
 qed.
 
 lemma composition_morphism:
- ∀A,B,C.∀U1,U2,U3.
-  ∀r1,r1':binary_relation A B U1 U2.
-   ∀r2,r2':binary_relation B C U2 U3.
+ ∀A,B,C.
+  ∀r1,r1':binary_relation A B.
+   ∀r2,r2':binary_relation B C.
     r1 = r1' → r2 = r2' → r1 ∘ r2 = r1' ∘ r2'.
- intros 14; split; intro;
+ intros 11; split; intro;
  cases H2; clear H2; cases H3; clear H3;
  [ lapply (if ?? (H x w) H2) | lapply (fi ?? (H x w) H2) ]
  [ lapply (if ?? (H1 w y) H4)| lapply (fi ?? (H1 w y) H4) ]
@@ -92,10 +85,10 @@ lemma composition_morphism:
  split; assumption.
 qed.
 
-definition binary_relation_setoid: ∀A,B. Ω \sup A → Ω \sup B → setoid.
- intros (A B U V);
+definition binary_relation_setoid: Type → Type → setoid.
+ intros (A B);
  constructor 1;
-  [ apply (binary_relation ?? U V)
+  [ apply (binary_relation A B)
   | constructor 1;
      [ apply equal_relations
      | apply refl_equal_relations
@@ -104,18 +97,11 @@ definition binary_relation_setoid: ∀A,B. Ω \sup A → Ω \sup B → setoid.
      ]]
 qed.
 
-record sigma (A:Type) (P: A → Type) : Type ≝
- { s_witness:> A;
-   s_proof:> P s_witness
- }.
-
-interpretation "sigma" 'sigma \eta.x = (sigma _ x).
-
 definition REL: category.
  constructor 1;
-  [ apply (ΣA:Type.Ω \sup A)
-  | intros; apply (binary_relation_setoid ?? (s_proof ?? s) (s_proof ?? s1))
-  | intros; constructor 1; intros; apply (s=s1) 
+  [ apply Type
+  | intros; apply (binary_relation_setoid T T1)
+  | intros; constructor 1; intros; apply (eq ? o1 o2);
   | intros; constructor 1;
      [ apply composition
      | apply composition_morphism
@@ -124,22 +110,16 @@ definition REL: category.
     apply associative_composition
   |6,7: intros 5; simplify; split; intro;
      [1,3: cases H; clear H; cases H1; clear H1;
-       [ rewrite > H | rewrite < H2 ]
+       [ alias id "eq_elim_r''" = "cic:/matita/logic/equality/eq_elim_r''.con".
+         apply (eq_elim_r'' ? w ?? x H); assumption
+       | alias id "eq_rect" = "cic:/matita/logic/equality/eq_rect.con".
+         apply (eq_rect ? w ?? y H2); assumption ]
        assumption
-     |*: exists; try assumption; split; first [ reflexivity | assumption ]]]
+     |*: exists; try assumption; split;
+         alias id "refl_eq" = "cic:/matita/logic/equality/eq.ind#xpointer(1/1/1)".
+         first [ apply refl_eq | assumption ]]]
 qed.
 
-definition elements: objs REL → Type ≝
- λb:ΣA.Ω\sup A.ssigma (s_witness ?? b) (s_proof ?? b).
-
-coercion elements.
-
-definition carrier: objs REL → Type ≝
- λb:ΣA.Ω\sup A.s_witness ?? b.
-
-interpretation "REL carrier" 'card c = (carrier c).
-
-definition subset: ∀b:objs REL. Ω \sup (carrier b) ≝
- λb:ΣA.Ω\sup A.s_proof ?? b.
+definition full_subset: ∀s:REL. Ω \sup s ≝ λs.{x | True}.
 
-coercion subset.
+coercion full_subset.
\ No newline at end of file