From da03907a38982b8b45459213f2b9581accac5143 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 3 Sep 2008 16:22:22 +0000
Subject: [PATCH] Setoids are now more pervasive.

---
 .../matita/library/datatypes/categories.ma    | 140 ++++++++++++++-
 .../matita/library/datatypes/subsets.ma       | 141 +++++++++++----
 .../library/formal_topology/basic_pairs.ma    |  60 +++----
 .../formal_topology/concrete_spaces.ma        | 118 +++++++++++--
 .../library/formal_topology/relations.ma      | 162 ++++++++----------
 5 files changed, 448 insertions(+), 173 deletions(-)

diff --git a/helm/software/matita/library/datatypes/categories.ma b/helm/software/matita/library/datatypes/categories.ma
index 0eb9b6818..e90e1457d 100644
--- a/helm/software/matita/library/datatypes/categories.ma
+++ b/helm/software/matita/library/datatypes/categories.ma
@@ -26,19 +26,90 @@ record setoid : Type ≝
    eq: equivalence_relation carr
  }.
 
+definition reflexive1 ≝ λA:Type.λR:A→A→CProp.∀x:A.R x x.
+definition symmetric1 ≝ λC:Type.λlt:C→C→CProp. ∀x,y:C.lt x y → lt y x.
+definition transitive1 ≝ λA:Type.λR:A→A→CProp.∀x,y,z:A.R x y → R y z → R x z.
+
+record equivalence_relation1 (A:Type) : Type ≝
+ { eq_rel1:2> A → A → CProp;
+   refl1: reflexive1 ? eq_rel1;
+   sym1: symmetric1 ? eq_rel1;
+   trans1: transitive1 ? eq_rel1
+ }.
+
+record setoid1: Type ≝
+ { carr1:> Type;
+   eq1: equivalence_relation1 carr1
+ }.
+
+definition setoid1_of_setoid: setoid → setoid1.
+ intro;
+ constructor 1;
+  [ apply (carr s)
+  | constructor 1;
+    [ apply (eq_rel s);
+      apply (eq s)
+    | apply (refl s)
+    | apply (sym s)
+    | apply (trans s)]]
+qed.
+
+coercion setoid1_of_setoid.
+
+(*
+definition Leibniz: Type → setoid.
+ intro;
+ constructor 1;
+  [ apply T
+  | constructor 1;
+     [ apply (λx,y:T.cic:/matita/logic/equality/eq.ind#xpointer(1/1) ? x y)
+     | alias id "refl_eq" = "cic:/matita/logic/equality/eq.ind#xpointer(1/1/1)".
+       apply refl_eq
+     | alias id "sym_eq" = "cic:/matita/logic/equality/sym_eq.con".
+       apply sym_eq
+     | alias id "trans_eq" = "cic:/matita/logic/equality/trans_eq.con".
+       apply trans_eq ]]
+qed.
+
+coercion Leibniz.
+*)
+
+interpretation "setoid1 eq" 'eq x y = (eq_rel1 _ (eq1 _) x y).
 interpretation "setoid eq" 'eq x y = (eq_rel _ (eq _) x y).
-notation ".= r" with precedence 50 for @{trans ????? $r}.
+interpretation "setoid1 symmetry" 'invert r = (sym1 ____ r).
 interpretation "setoid symmetry" 'invert r = (sym ____ r).
+notation ".= r" with precedence 50 for @{'trans $r}.
+interpretation "trans1" 'trans r = (trans1 _____ r).
+interpretation "trans" 'trans r = (trans _____ r).
 
-record binary_morphism (A,B,C: setoid) : Type ≝
+record unary_morphism (A,B: setoid1) : Type ≝
+ { fun_1:1> A → B;
+   prop_1: ∀a,a'. eq1 ? a a' → eq1 ? (fun_1 a) (fun_1 a')
+ }.
+
+record binary_morphism (A,B,C:setoid) : Type ≝
  { fun:2> A → B → C;
    prop: ∀a,a',b,b'. eq ? a a' → eq ? b b' → eq ? (fun a b) (fun a' b')
  }.
 
-notation "# r" with precedence 60 for @{prop ???????? (refl ???) $r}.
-notation "r #" with precedence 60 for @{prop ???????? $r (refl ???)}.
+record binary_morphism1 (A,B,C:setoid1) : Type ≝
+ { fun1:2> A → B → C;
+   prop1: ∀a,a',b,b'. eq1 ? a a' → eq1 ? b b' → eq1 ? (fun1 a b) (fun1 a' b')
+ }.
 
-definition CPROP: setoid.
+notation "hbox(a break ⇒ b)" right associative with precedence 20 for @{ 'Imply $a $b }.
+interpretation "unary morphism" 'Imply a b = (unary_morphism a b).
+
+notation "† c" with precedence 90 for @{'prop1 $c }.
+notation "l ‡ r" with precedence 90 for @{'prop $l $r }.
+notation "#" with precedence 90 for @{'refl}.
+interpretation "prop_1" 'prop1 c = (prop_1 _____ c).
+interpretation "prop1" 'prop l r = (prop1 ________ l r).
+interpretation "prop" 'prop l r = (prop ________ l r).
+interpretation "refl1" 'refl = (refl1 ___).
+interpretation "refl" 'refl = (refl ___).
+
+definition CPROP: setoid1.
  constructor 1;
   [ apply CProp
   | constructor 1;
@@ -49,6 +120,46 @@ definition CPROP: setoid.
         [ apply (H4 (H2 H6)) | apply (H3 (H5 H6))]]]
 qed.
 
+definition if': ∀A,B:CPROP. A = B → A → B.
+ intros; apply (if ?? H); assumption.
+qed.
+
+notation ". r" with precedence 50 for @{'if $r}.
+interpretation "if" 'if r = (if' __ r).
+
+definition and_morphism: binary_morphism1 CPROP CPROP CPROP.
+ constructor 1;
+  [ apply And
+  | intros; split; intro; cases H2; split;
+     [ apply (if ?? H a1)
+     | apply (if ?? H1 b1)
+     | apply (fi ?? H a1)
+     | apply (fi ?? H1 b1)]]
+qed.
+
+interpretation "and_morphism" 'and a b = (fun1 ___ and_morphism a b).
+
+definition or_morphism: binary_morphism1 CPROP CPROP CPROP.
+ constructor 1;
+  [ apply Or
+  | intros; split; intro; cases H2; [1,3:left |2,4: right]
+     [ apply (if ?? H a1)
+     | apply (fi ?? H a1)
+     | apply (if ?? H1 b1)
+     | apply (fi ?? H1 b1)]]
+qed.
+
+interpretation "or_morphism" 'or a b = (fun1 ___ or_morphism a b).
+
+definition if_morphism: binary_morphism1 CPROP CPROP CPROP.
+ constructor 1;
+  [ apply (λA,B. A → B)
+  | intros; split; intros;
+     [ apply (if ?? H1); apply H2; apply (fi ?? H); assumption
+     | apply (fi ?? H1); apply H2; apply (if ?? H); assumption]]
+qed.
+
+(*
 definition eq_morphism: ∀S:setoid. binary_morphism S S CPROP.
  intro;
  constructor 1;
@@ -61,6 +172,7 @@ definition eq_morphism: ∀S:setoid. binary_morphism S S CPROP.
        apply (.= H2);
        apply (H1 \sup -1)]]
 qed.
+*)
 
 record category : Type ≝
  { objs:> Type;
@@ -73,5 +185,21 @@ record category : Type ≝
    id_neutral_right: ∀o1,o2. ∀a: arrows o1 o2. comp ??? a (id o2) = a
  }.
 
+record category1 : Type ≝
+ { objs1:> Type;
+   arrows1: objs1 → objs1 → setoid1;
+   id1: ∀o:objs1. arrows1 o o;
+   comp1: ∀o1,o2,o3. binary_morphism1 (arrows1 o1 o2) (arrows1 o2 o3) (arrows1 o1 o3);
+   comp_assoc1: ∀o1,o2,o3,o4. ∀a12,a23,a34.
+    comp1 o1 o3 o4 (comp1 o1 o2 o3 a12 a23) a34 = comp1 o1 o2 o4 a12 (comp1 o2 o3 o4 a23 a34);
+   id_neutral_left1: ∀o1,o2. ∀a: arrows1 o1 o2. comp1 ??? (id1 o1) a = a;
+   id_neutral_right1: ∀o1,o2. ∀a: arrows1 o1 o2. comp1 ??? a (id1 o2) = a
+ }.
+
+notation "'ASSOC'" with precedence 90 for @{'assoc}.
+notation "'ASSOC1'" with precedence 90 for @{'assoc1}.
+
+interpretation "category1 composition" 'compose x y = (fun1 ___ (comp1 ____) x y).
+interpretation "category1 assoc" 'assoc1 = (comp_assoc1 ________).
 interpretation "category composition" 'compose x y = (fun ___ (comp ____) x y).
-notation "'ASSOC'" with precedence 90 for @{comp_assoc ????????}.
\ No newline at end of file
+interpretation "category assoc" 'assoc = (comp_assoc ________).
diff --git a/helm/software/matita/library/datatypes/subsets.ma b/helm/software/matita/library/datatypes/subsets.ma
index 26b449d74..5483dfa37 100644
--- a/helm/software/matita/library/datatypes/subsets.ma
+++ b/helm/software/matita/library/datatypes/subsets.ma
@@ -15,34 +15,113 @@
 include "logic/cprop_connectives.ma".
 include "datatypes/categories.ma".
 
-record powerset (A: Type) : Type ≝ { char: A → CProp }.
-
-interpretation "powerset" 'powerset A = (powerset A).
-
-interpretation "subset construction" 'subset \eta.x = (mk_powerset _ x).
-
-definition mem ≝ λA.λS:Ω \sup A.λx:A. match S with [mk_powerset c ⇒ c x].
-
-interpretation "mem" 'mem a S = (mem _ S a).
-
-definition overlaps ≝ λA:Type.λU,V:Ω \sup A.exT2 ? (λa:A. a ∈ U) (λa.a ∈ V).
-
-interpretation "overlaps" 'overlaps U V = (overlaps _ U V).
-
-definition subseteq ≝ λA:Type.λU,V:Ω \sup A.∀a:A. a ∈ U → a ∈ V.
-
-interpretation "subseteq" 'subseteq U V = (subseteq _ U V).
-
-definition intersects ≝ λA:Type.λU,V:Ω \sup A.{a | a ∈ U ∧ a ∈ V}.
-
-interpretation "intersects" 'intersects U V = (intersects _ U V).
-
-definition union ≝ λA:Type.λU,V:Ω \sup A.{a | a ∈ U ∨ a ∈ V}.
-
-interpretation "union" 'union U V = (union _ U V).
-
-include "logic/equality.ma".
-
-definition singleton ≝ λA:Type.λa:A.{b | a=b}.
-
-interpretation "singleton" 'singl a = (singleton _ a).
\ No newline at end of file
+record powerset_carrier (A: setoid) : Type ≝ { mem_operator: A ⇒ CPROP }.
+
+definition subseteq_operator ≝
+ λA:setoid.λU,V.∀a:A. mem_operator ? U a → mem_operator ? V a.
+
+theorem transitive_subseteq_operator: ∀A. transitive ? (subseteq_operator A).
+ intros 6; intros 2;
+ apply s1; apply s;
+ assumption.
+qed.
+
+definition powerset_setoid: setoid → setoid1.
+ intros (T);
+ constructor 1;
+  [ apply (powerset_carrier T)
+  | constructor 1;
+     [ apply (λU,V. subseteq_operator ? U V ∧ subseteq_operator ? V U)
+     | simplify; intros; split; intros 2; assumption
+     | simplify; intros (x y H); cases H; split; assumption
+     | simplify; intros (x y z H H1); cases H; cases H1; split;
+       apply transitive_subseteq_operator; [1,4: apply y ]
+       assumption ]]
+qed.
+
+interpretation "powerset" 'powerset A = (powerset_setoid A).
+
+interpretation "subset construction" 'subset \eta.x =
+ (mk_powerset_carrier _ (mk_unary_morphism _ CPROP x _)).
+
+definition mem: ∀A. binary_morphism1 A (Ω \sup A) CPROP.
+ intros;
+ constructor 1;
+  [ apply (λx,S. mem_operator ? S x)
+  | intros 5;
+    cases b; clear b; cases b'; clear b'; simplify; intros;
+    apply (trans1 ????? (prop_1 ?? u ?? H));
+    cases H1; whd in s s1;
+    split; intro;
+     [ apply s; assumption
+     | apply s1; assumption]]
+qed.     
+
+interpretation "mem" 'mem a S = (fun1 ___ (mem _) a S).
+
+definition subseteq: ∀A. binary_morphism1 (Ω \sup A) (Ω \sup A) CPROP.
+ intros;
+ constructor 1;
+  [ apply (λU,V. subseteq_operator ? U V)
+  | intros;
+    cases H; cases H1;
+    split; intros 1;
+    [ apply (transitive_subseteq_operator ????? s2);
+      apply (transitive_subseteq_operator ???? s1 s4)
+    | apply (transitive_subseteq_operator ????? s3);
+      apply (transitive_subseteq_operator ???? s s4) ]]
+qed.
+
+interpretation "subseteq" 'subseteq U V = (fun1 ___ (subseteq _) U V).
+
+definition overlaps: ∀A. binary_morphism1 (Ω \sup A) (Ω \sup A) CPROP.
+ intros;
+ constructor 1;
+  [ apply (λA.λU,V:Ω \sup A.exT2 ? (λx:A.x ∈ U) (λx:A.x ∈ V))
+  | intros;
+    constructor 1; intro; cases H2; exists; [1,4: apply w]
+     [ apply (. #‡H); assumption
+     | apply (. #‡H1); assumption
+     | apply (. #‡(H \sup -1)); assumption;
+     | apply (. #‡(H1 \sup -1)); assumption]]
+qed.
+
+interpretation "overlaps" 'overlaps U V = (fun1 ___ (overlaps _) U V).
+
+definition intersects:
+ ∀A. binary_morphism1 (powerset_setoid A) (powerset_setoid A) (powerset_setoid A).
+ intros;
+ constructor 1;
+  [ apply (λU,V. {x | x ∈ U ∧ x ∈ V });
+    intros; simplify; apply (.= (H‡#)‡(H‡#)); apply refl1;
+  | intros;
+    split; intros 2; simplify in f ⊢ %;
+    [ apply (. (#‡H)‡(#‡H1)); assumption
+    | apply (. (#‡(H \sup -1))‡(#‡(H1 \sup -1))); assumption]]
+qed.
+
+interpretation "intersects" 'intersects U V = (fun1 ___ (intersects _) U V).
+
+definition union:
+ ∀A. binary_morphism1 (powerset_setoid A) (powerset_setoid A) (powerset_setoid A).
+ intros;
+ constructor 1;
+  [ apply (λU,V. {x | x ∈ U ∨ x ∈ V });
+    intros; simplify; apply (.= (H‡#)‡(H‡#)); apply refl1
+  | intros;
+    split; intros 2; simplify in f ⊢ %;
+    [ apply (. (#‡H)‡(#‡H1)); assumption
+    | apply (. (#‡(H \sup -1))‡(#‡(H1 \sup -1))); assumption]]
+qed.
+
+interpretation "union" 'union U V = (fun1 ___ (union _) U V).
+
+definition singleton: ∀A:setoid. A → Ω \sup A.
+ apply (λA:setoid.λa:A.{b | a=b});
+ intros; simplify;
+ split; intro;
+ apply (.= H1);
+  [ apply H | apply (H \sup -1) ]
+qed.
+
+interpretation "singleton" 'singl a = (singleton _ a).
diff --git a/helm/software/matita/library/formal_topology/basic_pairs.ma b/helm/software/matita/library/formal_topology/basic_pairs.ma
index 7b1f97559..3ee864937 100644
--- a/helm/software/matita/library/formal_topology/basic_pairs.ma
+++ b/helm/software/matita/library/formal_topology/basic_pairs.ma
@@ -18,7 +18,7 @@ include "datatypes/categories.ma".
 record basic_pair: Type ≝
  { concr: REL;
    form: REL;
-   rel: arrows ? concr form
+   rel: arrows1 ? concr form
  }.
 
 notation "x ⊩ y" with precedence 45 for @{'Vdash2 $x $y}.
@@ -28,8 +28,8 @@ interpretation "basic pair relation" 'Vdash2 x y = (rel _ x y).
 interpretation "basic pair relation (non applied)" 'Vdash = (rel _).
 
 record relation_pair (BP1,BP2: basic_pair): Type ≝
- { concr_rel: arrows ? (concr BP1) (concr BP2);
-   form_rel: arrows ? (form BP1) (form BP2);
+ { concr_rel: arrows1 ? (concr BP1) (concr BP2);
+   form_rel: arrows1 ? (form BP1) (form BP2);
    commute: concr_rel ∘ ⊩ = ⊩ ∘ form_rel
  }.
 
@@ -40,23 +40,23 @@ interpretation "concrete relation" 'concr_rel r = (concr_rel __ r).
 interpretation "formal relation" 'form_rel r = (form_rel __ r). 
 
 definition relation_pair_equality:
- ∀o1,o2. equivalence_relation (relation_pair o1 o2).
+ ∀o1,o2. equivalence_relation1 (relation_pair o1 o2).
  intros;
  constructor 1;
   [ apply (λr,r'. r \sub\c ∘ ⊩ = r' \sub\c ∘ ⊩);
   | simplify;
     intros;
-    apply refl;
+    apply refl1;
   | simplify;
     intros 2;
-    apply sym;
+    apply sym1;
   | simplify;
     intros 3;
-    apply trans;
+    apply trans1;
   ]      
 qed.
 
-definition relation_pair_setoid: basic_pair → basic_pair → setoid.
+definition relation_pair_setoid: basic_pair → basic_pair → setoid1.
  intros;
  constructor 1;
   [ apply (relation_pair b b1)
@@ -66,7 +66,7 @@ qed.
 
 lemma eq_to_eq': ∀o1,o2.∀r,r': relation_pair_setoid o1 o2. r=r' → ⊩ \circ r \sub\f = ⊩ \circ r'\sub\f.
  intros 7 (o1 o2 r r' H c1 f2);
- split; intro;
+ split; intro H1;
   [ lapply (fi ?? (commute ?? r c1 f2) H1) as H2;
     lapply (if ?? (H c1 f2) H2) as H3;
     apply (if ?? (commute ?? r' c1 f2) H3);
@@ -79,15 +79,15 @@ qed.
 definition id: ∀o:basic_pair. relation_pair o o.
  intro;
  constructor 1;
-  [1,2: apply id;
-  | lapply (id_neutral_left ? (concr o) ? (⊩)) as H;
-    lapply (id_neutral_right ?? (form o) (⊩)) as H1;
+  [1,2: apply id1;
+  | lapply (id_neutral_left1 ? (concr o) ? (⊩)) as H;
+    lapply (id_neutral_right1 ?? (form o) (⊩)) as H1;
     apply (.= H);
     apply (H1 \sup -1);]
 qed.
 
 definition relation_pair_composition:
- ∀o1,o2,o3. binary_morphism (relation_pair_setoid o1 o2) (relation_pair_setoid o2 o3) (relation_pair_setoid o1 o3).
+ ∀o1,o2,o3. binary_morphism1 (relation_pair_setoid o1 o2) (relation_pair_setoid o2 o3) (relation_pair_setoid o1 o3).
  intros;
  constructor 1;
   [ intros (r r1);
@@ -96,26 +96,26 @@ definition relation_pair_composition:
      | apply (r \sub\f ∘ r1 \sub\f)
      | lapply (commute ?? r) as H;
        lapply (commute ?? r1) as H1;
-       apply (.= ASSOC);
-       apply (.= #H1);
-       apply (.= ASSOC\sup -1);
-       apply (.= H#);
-       apply comp_assoc]
+       apply (.= ASSOC1);
+       apply (.= #‡H1);
+       apply (.= ASSOC1\sup -1);
+       apply (.= H‡#);
+       apply ASSOC1]
   | intros;
     change with (a\sub\c ∘ b\sub\c ∘ ⊩ = a'\sub\c ∘ b'\sub\c ∘ ⊩);  
     change in H with (a \sub\c ∘ ⊩ = a' \sub\c ∘ ⊩);
     change in H1 with (b \sub\c ∘ ⊩ = b' \sub\c ∘ ⊩);
-    apply (.= ASSOC);
-    apply (.= #H1);
-    apply (.= #(commute ?? b'));
-    apply (.= ASSOC \sup -1);
-    apply (.= H#);
-    apply (.= ASSOC);
-    apply (.= #(commute ?? b')\sup -1);
-    apply (ASSOC \sup -1)]
+    apply (.= ASSOC1);
+    apply (.= #‡H1);
+    apply (.= #‡(commute ?? b'));
+    apply (.= ASSOC1 \sup -1);
+    apply (.= H‡#);
+    apply (.= ASSOC1);
+    apply (.= #‡(commute ?? b')\sup -1);
+    apply (ASSOC1 \sup -1)]
 qed.
     
-definition BP: category.
+definition BP: category1.
  constructor 1;
   [ apply basic_pair
   | apply relation_pair_setoid
@@ -124,12 +124,12 @@ definition BP: category.
   | intros;
     change with (a12\sub\c ∘ a23\sub\c ∘ a34\sub\c ∘ ⊩ =
                  (a12\sub\c ∘ (a23\sub\c ∘ a34\sub\c) ∘ ⊩));
-    apply (ASSOC#);
+    apply (ASSOC1‡#);
   | intros;
     change with ((id o1)\sub\c ∘ a\sub\c ∘ ⊩ = a\sub\c ∘ ⊩);
-    apply ((id_neutral_left ????)#);
+    apply ((id_neutral_left1 ????)‡#);
   | intros;
     change with (a\sub\c ∘ (id o2)\sub\c ∘ ⊩ = a\sub\c ∘ ⊩);
-    apply ((id_neutral_right ????)#);
+    apply ((id_neutral_right1 ????)‡#);
   ]
 qed.
\ No newline at end of file
diff --git a/helm/software/matita/library/formal_topology/concrete_spaces.ma b/helm/software/matita/library/formal_topology/concrete_spaces.ma
index ec32fca81..89665e5f9 100644
--- a/helm/software/matita/library/formal_topology/concrete_spaces.ma
+++ b/helm/software/matita/library/formal_topology/concrete_spaces.ma
@@ -14,28 +14,120 @@
 
 include "formal_topology/basic_pairs.ma".
 
-interpretation "REL carrier" 'card c = (carrier c).
-
-definition comprehension: ∀b:REL. (b → CProp) → Ω \sup |b| ≝
- λb:REL.λP.{x | ∃p: x ∈ b. P (mk_ssigma ?? x p)}.
+definition comprehension: ∀b:REL. (b ⇒ CPROP) → Ω \sup b.
+ apply (λb:REL. λP: b ⇒ CPROP. {x | x ∈ b ∧ P x});
+ intros; simplify; apply (.= (H‡#)‡(†H)); apply refl1.
+qed.
 
 interpretation "subset comprehension" 'comprehension s p =
- (comprehension s p).
+ (comprehension s (mk_unary_morphism __ p _)).
+
+definition ext: ∀X,S:REL. ∀r: arrows1 ? X S. S ⇒ Ω \sup X.
+ apply (λX,S,r.mk_unary_morphism ?? (λf.{x ∈ X | x ♮r f}) ?);
+  [ intros; simplify; apply (.= (H‡#)); apply refl1
+  | intros; simplify; split; intros; simplify; intros;
+     [ apply (. #‡(#‡H)); assumption
+     | apply (. #‡(#‡H\sup -1)); assumption]]
+qed.
 
-definition ext: ∀o: basic_pair. form o → Ω \sup |(concr o)| ≝
- λo,f.{x ∈ (concr o) | x ♮(rel o) f}.
+definition extS: ∀X,S:REL. ∀r: arrows1 ? X S. Ω \sup S ⇒ Ω \sup X.
+ (* ∃ is not yet a morphism apply (λX,S,r,F.{x ∈ X | ∃a. a ∈ F ∧ x ♮r a});*)
+ intros (X S r); constructor 1;
+  [ intro F; constructor 1; constructor 1;
+    [ apply (λx. x ∈ X ∧ ∃a:S. a ∈ F ∧ x ♮r a);
+    | intros; split; intro; cases f (H1 H2); clear f; split;
+       [ apply (. (H‡#)); assumption
+       |3: apply (. (H\sup -1‡#)); assumption
+       |2,4: cases H2 (w H3); exists; [1,3: apply w]
+         [ apply (. (#‡(H‡#))); assumption
+         | apply (. (#‡(H \sup -1‡#))); assumption]]]
+  | intros; split; simplify; intros; cases f; cases H1; split;
+     [1,3: assumption
+     |2,4: exists; [1,3: apply w]
+      [ apply (. (#‡H)‡#); assumption
+      | apply (. (#‡H\sup -1)‡#); assumption]]]
+qed.
 
-definition fintersects ≝
- λo: basic_pair.λa,b: form o.
-  {c | ext ? c ⊆ ext ? a ∩ ext ? b }.
+definition fintersects: ∀o: basic_pair. form o → form o → Ω \sup (form o).
+ apply
+  (λo: basic_pair.λa,b: form o.
+    {c | ext ?? (rel o) c ⊆ ext ?? (rel o) a ∩ ext ?? (rel o) b });
+ intros; simplify; apply (.= (†H)‡#); apply refl1.
+qed.
 
 interpretation "fintersects" 'fintersects U V = (fintersects _ U V).
+(*
+definition fintersectsS ≝
+ λo: basic_pair.λa,b: Ω \sup (form o).
+  {c | ext ?? (rel o) c ⊆ extS ?? (rel o) a ∩ extS ?? (rel o) b }.
+
+interpretation "fintersectsS" 'fintersects U V = (fintersectsS _ U V).
 
 definition relS: ∀o: basic_pair. concr o → Ω \sup (form o) → CProp ≝
- λo,x,S. ∃y. y ∈ S ∧ x ⊩ y.
+ λo,x,S. ∃y.y ∈ S ∧ x ⊩ y.
 
 interpretation "basic pair relation for subsets" 'Vdash2 x y = (relS _ x y).
 interpretation "basic pair relation for subsets (non applied)" 'Vdash = (relS _).
 
-definition convergence ≝
- λo: basic_pair.∀a: concr o.∀U,V: form o. a ⊩ U → a ⊩ V → a ⊩ (U ↓ V). 
\ No newline at end of file
+record concrete_space : Type ≝
+ { bp:> basic_pair;
+   converges: ∀a: concr bp.∀U,V: form bp. a ⊩ U → a ⊩ V → a ⊩ (U ↓ V);
+   all_covered: ∀x: concr bp. x ⊩ form bp
+ }.
+
+record convergent_relation_pair (CS1,CS2: concrete_space) : Type ≝
+ { rp:> relation_pair CS1 CS2;
+   respects_converges:
+    ∀b,c.
+     extS ?? rp \sub\c (extS ?? (rel CS2) (b ↓ c)) =
+     extS ?? (rel CS1) ((extS ?? rp \sub\f b) ↓ (extS ?? rp \sub\f c));
+   respects_all_covered:
+    extS ?? rp\sub\c (extS ?? (rel CS2) (form CS2)) =
+    extS ?? (rel CS1) (form CS1)
+ }.
+
+definition convergent_relation_space_setoid: concrete_space → concrete_space → setoid.
+ intros;
+ constructor 1;
+  [ apply (convergent_relation_pair c c1)
+  | constructor 1;
+     [ intros;
+       apply (relation_pair_equality c c1 c2 c3);
+     | intros 1; apply refl;
+     | intros 2; apply sym; 
+     | intros 3; apply trans]]
+qed.
+
+lemma equalset_extS_id_X_X: ∀o:REL.∀X.extS ?? (id ? o) X = X.
+ intros;
+ unfold extS;
+ split;
+  [ intros 2;
+    cases m; clear m;
+    cases H; clear H;
+    cases H1; clear H1;
+    whd in H;
+    apply (eq_elim_r'' ????? H);
+    assumption
+  | intros 2;
+    constructor 1;
+     [ whd; exact I 
+     | exists; [ apply a ]
+       split;
+        [ assumption
+        | whd; constructor 1]]]
+qed.
+
+definition CSPA: category.
+ constructor 1;
+  [ apply concrete_space
+  | apply convergent_relation_space_setoid
+  | intro; constructor 1;
+     [ apply id
+     | intros;
+       unfold id; simplify;
+       apply (.= (equalset_extS_id_X_X ??));
+
+     |
+     ]
+  |*)
\ No newline at end of file
diff --git a/helm/software/matita/library/formal_topology/relations.ma b/helm/software/matita/library/formal_topology/relations.ma
index 033788e92..e9989d4f7 100644
--- a/helm/software/matita/library/formal_topology/relations.ma
+++ b/helm/software/matita/library/formal_topology/relations.ma
@@ -14,112 +14,88 @@
 
 include "datatypes/subsets.ma".
 
-record binary_relation (A,B: Type) : Type ≝
- { satisfy:2> A → B → CProp }.
+record binary_relation (A,B: setoid) : Type ≝
+ { satisfy:> binary_morphism1 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 = (fun1 ___ (satisfy __ r) x y).
 
-definition composition:
- ∀A,B,C.
-  binary_relation A B → binary_relation B C →
-   binary_relation A C.
- intros (A B C R12 R23);
+definition binary_relation_setoid: setoid → setoid → setoid1.
+ intros (A B);
  constructor 1;
- intros (s1 s3);
- apply (∃s2. s1 ♮R12 s2 ∧ s2 ♮R23 s3);
-qed.
-
-interpretation "binary relation composition" 'compose x y = (composition ___ x y).
-
-definition equal_relations ≝
- λ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).
-
-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. 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. 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.
-  ∀r1:binary_relation A B.
-   ∀r2:binary_relation B C.
-    ∀r3:binary_relation C D.
-     (r1 ∘ r2) ∘ r3 = r1 ∘ (r2 ∘ r3).
- intros 9;
- split; intro;
- cases H; clear H; cases H1; clear H1;
- [cases H; clear H | cases H2; clear H2]
- cases H1; clear H1;
- exists; try assumption;
- split; try assumption;
- exists; try assumption;
- split; assumption.
+  [ apply (binary_relation A B)
+  | constructor 1;
+     [ apply (λA,B.λr,r': binary_relation A B. ∀x,y. r x y ↔ r' x y)
+     | simplify; intros 3; split; intro; assumption
+     | simplify; intros 5; split; intro;
+       [ apply (fi ?? (H ??)) | apply (if ?? (H ??))] assumption
+     | simplify;  intros 7; split; intro;
+        [ apply (if ?? (H1 ??)) | apply (fi ?? (H ??)) ]
+        [ apply (if ?? (H ??)) | apply (fi ?? (H1 ??)) ]
+       assumption]]
 qed.
 
-lemma composition_morphism:
+definition composition:
  ∀A,B,C.
-  ∀r1,r1':binary_relation A B.
-   ∀r2,r2':binary_relation B C.
-    r1 = r1' → r2 = r2' → r1 ∘ r2 = r1' ∘ r2'.
- 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) ]
- exists; try assumption;
- split; assumption.
-qed.
-
-definition binary_relation_setoid: Type → Type → setoid.
- intros (A B);
+  binary_morphism1 (binary_relation_setoid A B) (binary_relation_setoid B C) (binary_relation_setoid A C).
+ intros;
  constructor 1;
-  [ apply (binary_relation A B)
-  | constructor 1;
-     [ apply equal_relations
-     | apply refl_equal_relations
-     | apply sym_equal_relations
-     | apply trans_equal_relations
-     ]]
+  [ intros (R12 R23);
+    constructor 1;
+    constructor 1;
+     [ apply (λs1:A.λs3:C.∃s2:B. s1 ♮R12 s2 ∧ s2 ♮R23 s3);
+     | intros;
+       split; intro; cases H2 (w H3); clear H2; exists; [1,3: apply w ]
+        [ apply (. (H‡#)‡(#‡H1)); assumption
+        | apply (. ((H \sup -1)‡#)‡(#‡(H1 \sup -1))); assumption]]
+  | intros 8; split; intro H2; simplify in H2 ⊢ %;
+    cases H2 (w H3); clear H2; exists [1,3: apply w] cases H3 (H2 H4); 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) ]
+    exists; try assumption;
+    split; assumption]
 qed.
 
-definition REL: category.
+definition REL: category1.
  constructor 1;
-  [ apply Type
-  | intros; apply (binary_relation_setoid T T1)
-  | intros; constructor 1; intros; apply (eq ? o1 o2);
+  [ apply setoid
+  | intros (T T1); apply (binary_relation_setoid T T1)
   | intros; constructor 1;
-     [ apply composition
-     | apply composition_morphism
-     ]
-  | intros; unfold mk_binary_morphism; simplify;
-    apply associative_composition
-  |6,7: intros 5; simplify; split; intro;
-     [1,3: cases H; clear H; cases H1; clear H1;
-       [ 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;
-         alias id "refl_eq" = "cic:/matita/logic/equality/eq.ind#xpointer(1/1/1)".
-         first [ apply refl_eq | assumption ]]]
+    constructor 1; unfold setoid1_of_setoid; simplify;
+     [ intros; apply (c = c1)
+     | intros; split; intro;
+        [ apply (trans ????? (H \sup -1));
+          apply (trans ????? H2);
+          apply H1
+        | apply (trans ????? H);
+          apply (trans ????? H2);
+          apply (H1 \sup -1)]]
+  | apply composition
+  | intros 9;
+    split; intro;
+    cases f (w H); clear f; cases H; clear H;
+    [cases f (w1 H); clear f | cases f1 (w1 H); clear f1]
+    cases H; clear H;
+    exists; try assumption;
+    split; try assumption;
+    exists; try assumption;
+    split; assumption
+  |6,7: intros 5; unfold composition; simplify; split; intro;
+        unfold setoid1_of_setoid in x y; simplify in x y;
+        [1,3: cases H (w H1); clear H; cases H1; clear H1; unfold;
+          [ apply (. (H \sup -1 : eq1 ? w x)‡#); assumption
+          | apply (. #‡(H : eq1 ? w y)); assumption]
+        |2,4: exists; try assumption; split; first [apply refl | assumption]]]
 qed.
 
-definition full_subset: ∀s:REL. Ω \sup s ≝ λs.{x | True}.
+definition full_subset: ∀s:REL. Ω \sup s.
+ apply (λs.{x | True});
+ intros; simplify; split; intro; assumption.
+qed.
+
+coercion full_subset.
+
+definition setoid1_of_REL: REL → setoid ≝ λS. S.
 
-coercion full_subset.
\ No newline at end of file
+coercion setoid1_of_REL.
\ No newline at end of file
-- 
2.39.2