From cb98bd7054893edee16aadd6741ec5210b04afbc Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 15 Jan 2009 15:38:23 +0000
Subject: [PATCH] the new coercion behaviour (variants + composition with ID)
 and the new discipline of declaring hints for carrier of structures (setoids
 and categories) and no other hints simplified many passages

---
 .../formal_topology/overlap/basic_pairs.ma    | 23 +++--
 .../overlap/basic_topologies.ma               | 13 ---
 .../formal_topology/overlap/categories.ma     | 62 ++++++-------
 .../overlap/concrete_spaces.ma                | 16 ----
 .../overlap/cprop_connectives.ma              | 18 ++--
 .../overlap/formal_topologies.ma              | 25 -----
 .../formal_topology/overlap/o-algebra.ma      | 92 +++++--------------
 .../formal_topology/overlap/o-basic_pairs.ma  | 19 +++-
 .../o-basic_pairs_to_o-basic_topologies.ma    | 61 +++++-------
 .../overlap/o-basic_topologies.ma             | 62 +++++--------
 .../overlap/o-concrete_spaces.ma              | 57 +++++-------
 .../overlap/o-formal_topologies.ma            | 22 -----
 .../formal_topology/overlap/relations.ma      | 24 +++--
 .../overlap/relations_to_o-algebra.ma         | 46 ++++------
 .../overlap/saturations_to_o-saturations.ma   |  2 +-
 .../formal_topology/overlap/subsets.ma        |  4 +-
 16 files changed, 194 insertions(+), 352 deletions(-)

diff --git a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma b/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma
index 2635d51ce..a7be5cc6c 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma
@@ -20,11 +20,8 @@ record basic_pair: Type1 ≝
    rel: arrows1 ? concr form
  }.
 
-notation "x ⊩ y" with precedence 45 for @{'Vdash2 $x $y}.
-notation "⊩" with precedence 60 for @{'Vdash}.
-
-interpretation "basic pair relation" 'Vdash2 x y = (rel _ x y).
-interpretation "basic pair relation (non applied)" 'Vdash = (rel _).
+interpretation "basic pair relation" 'Vdash2 x y c = (fun21 ___ (rel c) x y).
+interpretation "basic pair relation (non applied)" 'Vdash c = (rel c).
 
 alias symbol "eq" = "setoid1 eq".
 alias symbol "compose" = "category1 composition".
@@ -65,7 +62,12 @@ definition relation_pair_setoid: basic_pair → basic_pair → setoid1.
   ]
 qed.
 
-lemma eq_to_eq': ∀o1,o2.∀r,r': relation_pair_setoid o1 o2. r=r' → r \sub\f ∘ ⊩ = r'\sub\f ∘ ⊩.
+definition relation_pair_of_relation_pair_setoid :
+  ∀P,Q. relation_pair_setoid P Q → relation_pair P Q ≝ λP,Q,x.x.
+coercion relation_pair_of_relation_pair_setoid.
+
+lemma eq_to_eq': 
+  ∀o1,o2.∀r,r':relation_pair_setoid o1 o2. r=r' → r \sub\f ∘ ⊩ = r'\sub\f ∘ ⊩.
  intros 7 (o1 o2 r r' H c1 f2);
  split; intro H1;
   [ lapply (fi ?? (commute ?? r c1 f2) H1) as H2;
@@ -139,6 +141,13 @@ definition BP: category1.
     apply ((id_neutral_left1 ????)‡#);]
 qed.
 
+definition basic_pair_of_BP : objs1 BP → basic_pair ≝ λx.x.
+coercion basic_pair_of_BP.
+
+definition relation_pair_setoid_of_arrows1_BP :
+  ∀P,Q. arrows1 BP P Q → relation_pair_setoid P Q ≝ λP,Q,x.x.
+coercion relation_pair_setoid_of_arrows1_BP.
+
 definition BPext: ∀o: BP. form o ⇒ Ω \sup (concr o).
  intros; constructor 1;
   [ apply (ext ? ? (rel o));
@@ -178,7 +187,7 @@ interpretation "fintersectsS" 'fintersects U V = (fun21 ___ (fintersectsS _) U V
 
 definition relS: ∀o: BP. binary_morphism1 (concr o) (Ω \sup (form o)) CPROP.
  intros (o); constructor 1;
-  [ apply (λx:concr o.λS: Ω \sup (form o).∃y:form o.y ∈ S ∧ x ⊩ y);
+  [ apply (λx:concr o.λS: Ω \sup (form o).∃y:form o.y ∈ S ∧ x ⊩_o y);
   | intros; split; intros; cases e2; exists [1,3: apply w]
      [ apply (. (#‡e1^-1)‡(e^-1‡#)); assumption
      | apply (. (#‡e1)‡(e‡#)); assumption]]
diff --git a/helm/software/matita/contribs/formal_topology/overlap/basic_topologies.ma b/helm/software/matita/contribs/formal_topology/overlap/basic_topologies.ma
index 4b53407d1..013ddb94d 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/basic_topologies.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/basic_topologies.ma
@@ -24,11 +24,6 @@ record basic_topology: Type1 ≝
    compatibility: ∀U,V. (A U ≬ J V) = (U ≬ J V)
  }.
 
-lemma hint: basic_topology → objs1 REL.
- intro; apply (carrbt b);
-qed.
-coercion hint.
-
 record continuous_relation (S,T: basic_topology) : Type1 ≝
  { cont_rel:> arrows1 ? S T;
    reduced: ∀U. U = J ? U → image ?? cont_rel U = J ? (image ?? cont_rel U);
@@ -45,14 +40,6 @@ definition continuous_relation_setoid: basic_topology → basic_topology → set
      | simplify; intros; apply trans1; [2: apply H |3: apply H1; |1: skip]]]
 qed.
 
-definition cont_rel': ∀S,T: basic_topology. continuous_relation_setoid S T → arrows1 ? S T ≝ cont_rel.
-
-coercion cont_rel'.
-
-definition cont_rel'': ∀S,T: basic_topology. continuous_relation_setoid S T → binary_relation S T ≝ cont_rel.
-
-coercion cont_rel''.
-
 theorem continuous_relation_eq':
  ∀o1,o2.∀a,a': continuous_relation_setoid o1 o2.
   a = a' → ∀X.minus_star_image ?? a (A o1 X) = minus_star_image ?? a' (A o1 X).
diff --git a/helm/software/matita/contribs/formal_topology/overlap/categories.ma b/helm/software/matita/contribs/formal_topology/overlap/categories.ma
index e22402d9f..c5db6ad60 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/categories.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/categories.ma
@@ -156,6 +156,9 @@ definition CPROP: setoid1.
         [ apply (f2 (f x1)) | apply (f1 (f3 z1))]]]
 qed.
 
+definition CProp0_of_CPROP: carr1 CPROP → CProp0 ≝ λx.x.
+coercion CProp0_of_CPROP.
+
 alias symbol "eq" = "setoid1 eq".
 definition fi': ∀A,B:CPROP. A = B → B → A.
  intros; apply (fi ?? e); assumption.
@@ -196,11 +199,12 @@ definition if_morphism: binary_morphism1 CPROP CPROP CPROP.
      | apply (fi ?? e1); apply f; apply (if ?? e); assumption]]
 qed.
 
+
 record category : Type1 ≝
  { objs:> Type0;
    arrows: objs → objs → setoid;
    id: ∀o:objs. arrows o o;
-   comp: ∀o1,o2,o3. binary_morphism1 (arrows o1 o2) (arrows o2 o3) (arrows o1 o3);
+   comp: ∀o1,o2,o3. binary_morphism (arrows o1 o2) (arrows o2 o3) (arrows o1 o3);
    comp_assoc: ∀o1,o2,o3,o4. ∀a12,a23,a34.
     comp o1 o3 o4 (comp o1 o2 o3 a12 a23) a34 = comp o1 o2 o4 a12 (comp o2 o3 o4 a23 a34);
    id_neutral_left: ∀o1,o2. ∀a: arrows o1 o2. comp ??? (id o1) a = a;
@@ -252,9 +256,9 @@ qed.
 definition SET: category1.
  constructor 1;
   [ apply setoid;
-  | apply rule (λS,T:setoid.unary_morphism_setoid S T);
+  | apply rule (λS,T:setoid.setoid1_of_setoid (unary_morphism_setoid S T));
   | intros; constructor 1; [ apply (λx:carr o.x); | intros; assumption ]
-  | intros; constructor 1; [ intros; constructor 1; [ apply (λx. t1 (t x)); | intros;
+  | intros; constructor 1; [ intros; constructor 1; [ apply (λx. c1 (c x)); | intros;
      apply († (†e));]
   | intros; whd; intros; simplify; whd in H1; whd in H;
     apply trans; [ apply (b (a' a1)); | lapply (prop1 ?? b (a a1) (a' a1));
@@ -265,10 +269,13 @@ definition SET: category1.
   ]
 qed.
 
-definition setoid_of_SET: objs1 SET → setoid.
- intros; apply o; qed.
+definition setoid_of_SET: objs1 SET → setoid ≝ λx.x.
 coercion setoid_of_SET.
 
+definition unary_morphism_setoid_of_arrows1_SET: 
+  ∀P,Q.arrows1 SET P Q → unary_morphism_setoid P Q  ≝ λP,Q,x.x.
+coercion unary_morphism_setoid_of_arrows1_SET.
+
 notation "hbox(a break ⇒ b)" right associative with precedence 20 for @{ 'Imply $a $b }.
 interpretation "unary morphism" 'Imply a b = (arrows1 SET a b).
 
@@ -285,12 +292,16 @@ definition unary_morphism1_setoid1: setoid1 → setoid1 → setoid1.
      | simplify; intros; apply trans1; [2: apply f; | skip | apply f1]]]
 qed.
 
+definition unary_morphism1_of_unary_morphism1_setoid1 : 
+  ∀S,T. unary_morphism1_setoid1 S T → unary_morphism1 S T ≝ λP,Q,x.x.
+coercion unary_morphism1_of_unary_morphism1_setoid1.
+
 definition SET1: category2.
  constructor 1;
   [ apply setoid1;
-  | apply rule (λS,T.unary_morphism1_setoid1 S T);
+  | apply rule (λS,T.setoid2_of_setoid1 (unary_morphism1_setoid1 S T));
   | intros; constructor 1; [ apply (λx.x); | intros; assumption ]
-  | intros; constructor 1; [ intros; constructor 1; [ apply (λx. t1 (t x)); | intros;
+  | intros; constructor 1; [ intros; constructor 1; [ apply (λx. c1 (c x)); | intros;
      apply († (†e));]
   | intros; whd; intros; simplify; whd in H1; whd in H;
     apply trans1; [ apply (b (a' a1)); | lapply (prop11 ?? b (a a1) (a' a1));
@@ -301,36 +312,17 @@ definition SET1: category2.
   ]
 qed.
 
-definition setoid1_OF_SET1: objs2 SET1 → setoid1.
- intros; apply o; qed.
+definition setoid1_of_SET1: objs2 SET1 → setoid1 ≝ λx.x.
+coercion setoid1_of_SET1.
 
-coercion setoid1_OF_SET1.
+definition unary_morphism1_setoid1_of_arrows2_SET1: 
+  ∀P,Q.arrows2 SET1 P Q → unary_morphism1_setoid1 P Q ≝ λP,Q,x.x.
+coercion unary_morphism1_setoid1_of_arrows2_SET1.
  
-definition setoid2_OF_category2: Type_OF_category2 SET1 → setoid2.
- intro; apply (setoid2_of_setoid1 t); qed.
-coercion setoid2_OF_category2.
-
-definition objs2_OF_category1: Type_OF_category1 SET → objs2 SET1.
- intro; apply (setoid1_of_setoid t); qed.
-coercion objs2_OF_category1.
+variant objs2_of_category1: objs1 SET → objs2 SET1 ≝ setoid1_of_setoid.
+coercion objs2_of_category1.
 
-definition Type1_OF_SET1: Type_OF_category2 SET1 → Type1.
- intro; whd in t; apply (carr1 t);
-qed.
-coercion Type1_OF_SET1.
-
-definition Type_OF_setoid1_of_carr: ∀U. carr U → Type_OF_setoid1 ?(*(setoid1_of_SET U)*).
- [ apply rule U; 
- | intros; apply c;]
-qed.
-coercion Type_OF_setoid1_of_carr.
-
-definition carr' ≝ λx:Type_OF_category1 SET.Type_OF_Type0 (carr x).
-coercion carr'. (* we prefer the lower carrier projection *)
+prefer coercion Type_OF_setoid. (* we prefer the lower carrier projection *)
+prefer coercion Type_OF_objs1.
 
 interpretation "unary morphism1" 'Imply a b = (arrows2 SET1 a b).
-
-lemma unary_morphism1_of_arrows1_SET1: ∀S,T. (S ⇒ T) → unary_morphism1 S T.
- intros; apply t;
-qed.
-coercion unary_morphism1_of_arrows1_SET1.
diff --git a/helm/software/matita/contribs/formal_topology/overlap/concrete_spaces.ma b/helm/software/matita/contribs/formal_topology/overlap/concrete_spaces.ma
index 5ce337c6f..07a067e73 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/concrete_spaces.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/concrete_spaces.ma
@@ -21,12 +21,6 @@ record concrete_space : Type1 ≝
    all_covered: ∀x: concr bp. x ⊩ full_subset (form bp)
  }.
 
-definition bp': concrete_space → basic_pair ≝ λc.bp c.
-coercion bp'.
-
-definition bp'': concrete_space → objs1 BP ≝ λc.bp c.
-coercion bp''.
-
 record convergent_relation_pair (CS1,CS2: concrete_space) : Type1 ≝
  { rp:> arrows1 ? CS1 CS2;
    respects_converges:
@@ -37,11 +31,6 @@ record convergent_relation_pair (CS1,CS2: concrete_space) : Type1 ≝
     minus_image ?? rp\sub\c (BPextS CS2 (full_subset (form CS2))) = BPextS CS1 (full_subset (form CS1))
  }.
 (*
-definition rp' : ∀CS1,CS2. convergent_relation_pair CS1 CS2 → relation_pair CS1 CS2 ≝
- λCS1,CS2,c. rp CS1 CS2 c.
- 
-coercion rp'.
-
 definition convergent_relation_space_setoid: concrete_space → concrete_space → setoid1.
  intros;
  constructor 1;
@@ -54,11 +43,6 @@ definition convergent_relation_space_setoid: concrete_space → concrete_space 
      | intros 3; apply trans1]]
 qed.
 
-definition rp'': ∀CS1,CS2.convergent_relation_space_setoid CS1 CS2 → arrows1 BP CS1 CS2 ≝
- λCS1,CS2,c.rp ?? c.
-
-coercion rp''.
-
 definition convergent_relation_space_composition:
  ∀o1,o2,o3: concrete_space.
   binary_morphism1
diff --git a/helm/software/matita/contribs/formal_topology/overlap/cprop_connectives.ma b/helm/software/matita/contribs/formal_topology/overlap/cprop_connectives.ma
index aff6849b3..d6c7084b0 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/cprop_connectives.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/cprop_connectives.ma
@@ -19,14 +19,14 @@ definition Type2 : Type3 := Type.
 definition Type1 : Type2 := Type.
 definition Type0 : Type1 := Type.
 
-definition Type_OF_Type0: Type0 → Type := λx.x.
-definition Type_OF_Type1: Type1 → Type := λx.x.
-definition Type_OF_Type2: Type2 → Type := λx.x.
-definition Type_OF_Type3: Type3 → Type := λx.x.
-coercion Type_OF_Type0.
-coercion Type_OF_Type1.
-coercion Type_OF_Type2.
-coercion Type_OF_Type3.
+definition Type_of_Type0: Type0 → Type := λx.x.
+definition Type_of_Type1: Type1 → Type := λx.x.
+definition Type_of_Type2: Type2 → Type := λx.x.
+definition Type_of_Type3: Type3 → Type := λx.x.
+coercion Type_of_Type0.
+coercion Type_of_Type1.
+coercion Type_of_Type2.
+coercion Type_of_Type3.
 
 definition CProp0 : Type1 := Type0.
 definition CProp1 : Type2 := Type1.
@@ -148,4 +148,4 @@ definition antisymmetric: ∀A:Type0. ∀R:A→A→CProp0. ∀eq:A→A→Prop.CP
 
 definition reflexive: ∀C:Type0. ∀lt:C→C→CProp0.CProp0 ≝ λA:Type0.λR:A→A→CProp0.∀x:A.R x x.
 
-definition transitive: ∀C:Type0. ∀lt:C→C→CProp0.CProp0 ≝ λA:Type0.λR:A→A→CProp0.∀x,y,z:A.R x y → R y z → R x z.
\ No newline at end of file
+definition transitive: ∀C:Type0. ∀lt:C→C→CProp0.CProp0 ≝ λA:Type0.λR:A→A→CProp0.∀x,y,z:A.R x y → R y z → R x z.
diff --git a/helm/software/matita/contribs/formal_topology/overlap/formal_topologies.ma b/helm/software/matita/contribs/formal_topology/overlap/formal_topologies.ma
index eb2b0b1f7..a611e22ea 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/formal_topologies.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/formal_topologies.ma
@@ -14,13 +14,6 @@
 
 include "basic_topologies.ma".
 
-definition btop_carr: BTop → Type ≝ λo:BTop. carr (carrbt o).
-
-coercion btop_carr.
-
-definition btop_carr': BTop → setoid ≝ λo:BTop. carrbt o.
-
-coercion btop_carr'.
 
 definition downarrow: ∀S:BTop. unary_morphism (Ω \sup S) (Ω \sup S).
  intros; constructor 1;
@@ -46,9 +39,6 @@ record formal_topology: Type ≝
    converges: ∀U,V: Ω \sup bt. A ? (U ↓ V) = A ? U ∩ A ? V
  }.
 
-definition bt': formal_topology → basic_topology ≝ λo:formal_topology.bt o.
-
-coercion bt'.
 
 definition ffintersects': ∀S:BTop. binary_morphism1 S S (Ω \sup S).
  intros; constructor 1;
@@ -64,11 +54,6 @@ record formal_map (S,T: formal_topology) : Type ≝
    C2: extS ?? cr T = S
  }.
 
-definition cr': ∀FT1,FT2.formal_map FT1 FT2 → continuous_relation FT1 FT2 ≝
- λFT1,FT2,c. cr FT1 FT2 c.
-
-coercion cr'.
-
 definition formal_map_setoid: formal_topology → formal_topology → setoid1.
  intros (S T); constructor 1;
   [ apply (formal_map S T);
@@ -79,16 +64,6 @@ definition formal_map_setoid: formal_topology → formal_topology → setoid1.
      | simplify; intros 3; apply trans1]]
 qed.
 
-definition cr'': ∀FT1,FT2.formal_map_setoid FT1 FT2 → arrows1 BTop FT1 FT2 ≝
- λFT1,FT2,c.cr ?? c.
-
-coercion cr''.
-
-definition cr''': ∀FT1,FT2.formal_map_setoid FT1 FT2 → arrows1 REL FT1 FT2 ≝
- λFT1,FT2:formal_topology.λc:formal_map_setoid FT1 FT2.cont_rel FT1 FT2 (cr' ?? c).
-
-coercion cr'''.
-
 axiom C1':
  ∀S,T: formal_topology.∀f:formal_map_setoid S T.∀U,V: Ω \sup T.
   extS ?? f (U ↓ V) = extS ?? f U ↓ extS ?? f V.
diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma b/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma
index ca3d0379b..41f9bfd0e 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma
@@ -63,7 +63,9 @@ record OAlgebra : Type2 := {
   oa_leq_antisym: ∀a,b:oa_P.oa_leq a b → oa_leq b a → a = b;
   oa_leq_trans: ∀a,b,c:oa_P.oa_leq a b → oa_leq b c → oa_leq a c;
   oa_overlap_sym: ∀a,b:oa_P.oa_overlap a b → oa_overlap b a;
-  oa_meet_inf: ∀I:SET.∀p_i:I ⇒ oa_P.∀p:oa_P.oa_leq p (oa_meet I p_i) = ∀i:I.oa_leq p (p_i i);
+  oa_meet_inf: 
+    ∀I:SET.∀p_i:I ⇒ oa_P.∀p:oa_P.
+      oa_leq p (oa_meet I p_i) = ∀i:I.oa_leq p (p_i i);
   oa_join_sup: ∀I:SET.∀p_i:I ⇒ oa_P.∀p:oa_P.oa_leq (oa_join I p_i) p = ∀i:I.oa_leq (p_i i) p;
   oa_zero_bot: ∀p:oa_P.oa_leq oa_zero p;
   oa_one_top: ∀p:oa_P.oa_leq p oa_one;
@@ -113,16 +115,6 @@ interpretation "o-algebra join" 'oa_join f =
 interpretation "o-algebra join with explicit function" 'oa_join_mk f = 
   (fun12 __ (oa_join __) (mk_unary_morphism _ _ f _)).
 
-definition hint3: OAlgebra → setoid1.
- intro; apply (oa_P o);
-qed.
-coercion hint3.
-
-definition hint4: ∀A. setoid2_OF_OAlgebra A → hint3 A.
- intros; apply t;
-qed.
-coercion hint4.
-
 definition binary_meet : ∀O:OAlgebra. binary_morphism1 O O O.
 intros; split;
 [ intros (p q); 
@@ -178,16 +170,11 @@ interpretation "o-algebra join" 'oa_join f =
 interpretation "o-algebra join with explicit function" 'oa_join_mk f = 
   (fun12 __ (oa_join __) (mk_unary_morphism _ _ f _)).
 
-definition hint5: OAlgebra → objs2 SET1.
- intro; apply (oa_P o);
-qed.
-coercion hint5.
-
 record ORelation (P,Q : OAlgebra) : Type2 ≝ {
-  or_f_ : P ⇒ Q;
-  or_f_minus_star_ : P ⇒ Q;
-  or_f_star_ : Q ⇒ P;
-  or_f_minus_ : Q ⇒ P;
+  or_f_ : carr2 (P ⇒ Q);
+  or_f_minus_star_ : carr2(P ⇒ Q);
+  or_f_star_ : carr2(Q ⇒ P);
+  or_f_minus_ : carr2(Q ⇒ P);
   or_prop1_ : ∀p,q. (or_f_ p ≤ q) = (p ≤ or_f_star_ q);
   or_prop2_ : ∀p,q. (or_f_minus_ p ≤ q) = (p ≤ or_f_minus_star_ q);
   or_prop3_ : ∀p,q. (or_f_ p >< q) = (p >< or_f_minus_ q)
@@ -214,6 +201,10 @@ constructor 1;
      | apply (.= (e3 a)); apply e7;]]]
 qed.
 
+definition ORelation_of_ORelation_setoid : 
+  ∀P,Q.ORelation_setoid P Q → ORelation P Q ≝ λP,Q,x.x.
+coercion ORelation_of_ORelation_setoid.
+
 definition or_f_minus_star:
  ∀P,Q:OAlgebra.unary_morphism2 (ORelation_setoid P Q) (P ⇒ Q).
  intros; constructor 1;
@@ -227,8 +218,6 @@ definition or_f: ∀P,Q:OAlgebra.unary_morphism2 (ORelation_setoid P Q) (P ⇒ Q
   | intros; cases e; assumption]
 qed.
 
-coercion or_f.
-
 definition or_f_minus: ∀P,Q:OAlgebra.unary_morphism2 (ORelation_setoid P Q) (Q ⇒ P).
  intros; constructor 1;
   [ apply or_f_minus_;
@@ -241,36 +230,10 @@ definition or_f_star: ∀P,Q:OAlgebra.unary_morphism2 (ORelation_setoid P Q) (Q
   | intros; cases e; assumption]
 qed.
 
-lemma arrows1_OF_ORelation_setoid : ∀P,Q. ORelation_setoid P Q → (P ⇒ Q).
-intros; apply (or_f ?? t);
-qed.
-
-coercion arrows1_OF_ORelation_setoid.
-
-lemma umorphism_OF_ORelation_setoid : ∀P,Q. ORelation_setoid P Q → unary_morphism1 P Q.
-intros; apply (or_f ?? t);
+lemma arrows1_of_ORelation_setoid : ∀P,Q. ORelation_setoid P Q → (P ⇒ Q). 
+intros; apply (or_f ?? c);
 qed.
-
-coercion umorphism_OF_ORelation_setoid.
-
-lemma umorphism_setoid_OF_ORelation_setoid : ∀P,Q. ORelation_setoid P Q → unary_morphism1_setoid1 P Q.
-intros; apply (or_f ?? t);
-qed.
-
-coercion umorphism_setoid_OF_ORelation_setoid.
-
-lemma uncurry_arrows : ∀B,C. ORelation_setoid B C → B → C. 
-intros; apply (t t1);
-qed.
-
-coercion uncurry_arrows 1.
-
-(*
-lemma hint6: ∀P,Q. Type_OF_setoid2 (hint5 P ⇒ hint5 Q) → unary_morphism1 P Q.
- intros; apply t;
-qed.
-coercion hint6.
-*)
+coercion arrows1_of_ORelation_setoid.
 
 notation "r \sup *" non associative with precedence 90 for @{'OR_f_star $r}.
 notation > "r *" non associative with precedence 90 for @{'OR_f_star $r}.
@@ -323,7 +286,9 @@ constructor 1;
     apply or_prop3;
   ]
 | intros; split; simplify; 
-   [1,3: unfold umorphism_setoid_OF_ORelation_setoid; unfold arrows1_OF_ORelation_setoid; apply ((†e)‡(†e1));
+   [3: unfold arrows1_of_ORelation_setoid;
+         apply ((†e)‡(†e1));
+   |1: apply ((†e)‡(†e1));
    |2,4: apply ((†e1)‡(†e));]]
 qed.
 
@@ -345,22 +310,11 @@ split;
 | intros; split; unfold ORelation_composition; simplify; apply id_neutral_right2;]
 qed.
 
-lemma setoid1_of_OA: OA → setoid1.
- intro; apply (oa_P t);
-qed.
-coercion setoid1_of_OA.
-
-lemma SET1_of_OA: OA → SET1.
- intro; whd; apply (setoid1_of_OA t);
-qed.
-coercion SET1_of_OA.
+definition OAlgebra_of_objs2_OA: objs2 OA → OAlgebra ≝ λx.x.
+coercion OAlgebra_of_objs2_OA.
 
-lemma objs2_SET1_OF_OA: OA → objs2 SET1.
- intro; whd; apply (setoid1_of_OA t);
-qed.
-coercion objs2_SET1_OF_OA.
+definition ORelation_setoid_of_arrows2_OA: 
+  ∀P,Q. arrows2 OA P Q → ORelation_setoid P Q ≝ λP,Q,c.c.
+coercion ORelation_setoid_of_arrows2_OA.
 
-lemma Type_OF_category2_OF_SET1_OF_OA: OA → Type_OF_category2 SET1.
- intro; apply (oa_P t);
-qed.
-coercion Type_OF_category2_OF_SET1_OF_OA.
+prefer coercion Type_OF_objs2.
\ No newline at end of file
diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma b/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma
index 956a26af9..6517689a1 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs.ma
@@ -20,16 +20,15 @@ record basic_pair: Type2 ≝
    rel: arrows2 ? concr form
  }.
 
-notation > "x ⊩ y" with precedence 45 for @{'Vdash2 $x $y ?}.
-notation < "x (⊩  \below c) y" with precedence 45 for @{'Vdash2 $x $y $c}.
-notation < "⊩ \sub c" with precedence 60 for @{'Vdash $c}.
-notation > "⊩ " with precedence 60 for @{'Vdash ?}.
-
 interpretation "basic pair relation indexed" 'Vdash2 x y c = (rel c x y).
 interpretation "basic pair relation (non applied)" 'Vdash c = (rel c).
 
 alias symbol "eq" = "setoid1 eq".
 alias symbol "compose" = "category1 composition".
+(*DIFFER*)
+
+alias symbol "eq" = "setoid2 eq".
+alias symbol "compose" = "category2 composition".
 record relation_pair (BP1,BP2: basic_pair): Type2 ≝
  { concr_rel: arrows2 ? (concr BP1) (concr BP2);
    form_rel: arrows2 ? (form BP1) (form BP2);
@@ -68,6 +67,10 @@ definition relation_pair_setoid: basic_pair → basic_pair → setoid2.
   ]
 qed.
 
+definition relation_pair_of_relation_pair_setoid: 
+  ∀P,Q. relation_pair_setoid P Q → relation_pair P Q ≝ λP,Q,x.x.
+coercion relation_pair_of_relation_pair_setoid.
+
 lemma eq_to_eq': ∀o1,o2.∀r,r': relation_pair_setoid o1 o2. r=r' → r \sub\f ∘ ⊩ = r'\sub\f ∘ ⊩.
  intros 5 (o1 o2 r r' H); change in H with (⊩ ∘ r\sub\c = ⊩ ∘ r'\sub\c);
  apply (.= ((commute ?? r) \sup -1));
@@ -134,6 +137,12 @@ definition BP: category2.
     apply ((id_neutral_left2 ????)‡#);]
 qed.
 
+definition basic_pair_of_objs2_BP: objs2 BP → basic_pair ≝ λx.x.
+coercion basic_pair_of_objs2_BP.
+
+definition relation_pair_setoid_of_arrows2_BP: 
+  ∀P,Q.arrows2 BP P Q → relation_pair_setoid P Q ≝ λP,Q,c.c.
+coercion relation_pair_setoid_of_arrows2_BP.
 
 (*
 definition BPext: ∀o: BP. form o ⇒ Ω \sup (concr o).
diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs_to_o-basic_topologies.ma b/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs_to_o-basic_topologies.ma
index f2f6af020..c66e709dd 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs_to_o-basic_topologies.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/o-basic_pairs_to_o-basic_topologies.ma
@@ -15,8 +15,10 @@
 include "o-basic_pairs.ma".
 include "o-basic_topologies.ma".
 
+alias symbol "eq" = "setoid1 eq".
+
 (* qui la notazione non va *)
-lemma leq_to_eq_join: ∀S:OA.∀p,q:S. p ≤ q → q = binary_join ? p q.
+lemma leq_to_eq_join: ∀S:OA.∀p,q:S. p ≤ q → q = (binary_join ? p q).
  intros;
  apply oa_leq_antisym;
   [ apply oa_density; intros;
@@ -126,18 +128,12 @@ lemma lemma_10_3_d: ∀S,T.∀R:arrows2 OA S T.∀p. R⎻* (R⎻ (R⎻* p)) = R
 qed.
 
 lemma lemma_10_4_a: ∀S,T.∀R:arrows2 OA S T.∀p. R⎻* (R⎻ (R⎻* (R⎻ p))) = R⎻* (R⎻ p).
- intros;
- (* BAD *)
- lapply (†(lemma_10_3_a ?? R p)); [2: apply (R⎻* ); | skip | apply Hletin ]
+ intros; apply (†(lemma_10_3_a ?? R p));
 qed.
 
-(* VEERY BAD! *)
-axiom lemma_10_4_b: ∀S,T.∀R:arrows2 OA S T.∀p. R (R* (R (R* p))) = R (R* p).
-(*
- intros;
- (* BAD *)
- lapply (†(lemma_10_3_b ?? R p)); [2: apply rule R; | skip | apply Hletin ]
-qed. *)
+lemma lemma_10_4_b: ∀S,T.∀R:arrows2 OA S T.∀p. R (R* (R (R* p))) = R (R* p).
+intros; unfold in ⊢ (? ? ? % %); apply (†(lemma_10_3_b ?? R p));
+qed.
 
 lemma oa_overlap_sym': ∀o:OA.∀U,V:o. (U >< V) = (V >< U).
  intros; split; intro; apply oa_overlap_sym; assumption.
@@ -145,7 +141,7 @@ qed.
 
 (* Qui, per fare le cose per bene, ci serve la nozione di funtore categorico *)
 definition o_basic_topology_of_o_basic_pair: BP → BTop.
- intro;
+ intro t;
  constructor 1;
   [ apply (form t);
   | apply (□_t ∘ Ext⎽t);
@@ -186,42 +182,35 @@ qed.
 definition o_continuous_relation_of_o_relation_pair:
  ∀BP1,BP2.arrows2 BP BP1 BP2 →
   arrows2 BTop (o_basic_topology_of_o_basic_pair BP1) (o_basic_topology_of_o_basic_pair BP2).
- intros;
+ intros (BP1 BP2 t);
  constructor 1;
   [ apply (t \sub \f);
   | unfold o_basic_topology_of_o_basic_pair; simplify; intros;
     apply sym1;
-    alias symbol "refl" = "refl1".
-    apply (.= †?); [1: apply (t \sub \f (((◊_BP1∘(⊩)* ) U))); |
-    lapply (†e); [2: apply rule t \sub \f; | skip | apply Hletin]]
-    change in ⊢ (? ? ? % ?) with ((◊_BP2 ∘(⊩)* ) ((t \sub \f ∘ (◊_BP1∘(⊩)* )) U));
-    lapply (comp_assoc2 ????? (⊩)* (⊩) t \sub \f);
-    apply (.= †(Hletin ?)); clear Hletin;
+    unfold in ⊢ (? ? ? (? ? ? ? %) ?);
+    apply (.= †(†e));
     change in ⊢ (? ? ? (? ? ? ? %) ?) with ((t \sub \f ∘ (⊩)) ((⊩)* U));
-    cut ?;
-     [3: apply CProp1; |5: cases (commute ?? t); [2: apply (e3 ^ -1 ((⊩)* U));] | 2,4: skip]
-    apply (.= †Hcut);
+    cut ((t \sub \f ∘ (⊩)) ((⊩)* U) = ((⊩) ∘ t \sub \c) ((⊩)* U)) as COM;[2:
+      cases (commute ?? t); apply (e3 ^ -1 ((⊩)* U));]
+    apply (.= †COM);
     change in ⊢ (? ? ? % ?) with (((⊩) ∘ (⊩)* ) (((⊩) ∘ t \sub \c ∘ (⊩)* ) U));
     apply (.= (lemma_10_3_c ?? (⊩) (t \sub \c ((⊩)* U))));
-    apply (.= Hcut ^ -1);
+    apply (.= COM ^ -1);
     change in ⊢ (? ? ? % ?) with (t \sub \f (((⊩) ∘ (⊩)* ) U));
-    apply (prop11 ?? t \sub \f);
-    apply (e ^ -1);
+    change in e with (U=((⊩)∘(⊩ \sub BP1) \sup * ) U);
+    unfold in ⊢ (? ? ? % %); apply (†e^-1);
   | unfold o_basic_topology_of_o_basic_pair; simplify; intros;
     apply sym1;
-    apply (.= †?); [1: apply (t \sub \f⎻* ((((⊩)⎻* ∘ (⊩)⎻) U))); |
-    lapply (†e); [2: apply rule (t \sub \f⎻* ); | skip | apply Hletin]]
-    change in ⊢ (? ? ? % ?) with (((⊩)⎻* ∘(⊩)⎻ ) ((t \sub \f⎻* ∘ ((⊩)⎻*∘(⊩)⎻ )) U));
-    lapply (comp_assoc2 ????? (⊩)⎻ (⊩)⎻* t \sub \f⎻* );
-    apply (.= †(Hletin ?)); clear Hletin;
+    unfold in ⊢ (? ? ? (? ? ? ? %) ?);
+    apply (.= †(†e));
     change in ⊢ (? ? ? (? ? ? ? %) ?) with ((t \sub \f⎻* ∘ (⊩)⎻* ) ((⊩)⎻ U));
-    cut ?;
-     [3: apply CProp1; |5: cases (commute ?? t); [2: apply (e1 ^ -1 ((⊩)⎻ U));] | 2,4: skip]
-    apply (.= †Hcut);
+    cut ((t \sub \f⎻* ∘ (⊩)⎻* ) ((⊩)⎻ U) = ((⊩)⎻* ∘ t \sub \c⎻* ) ((⊩)⎻ U)) as COM;[2:
+      cases (commute ?? t); apply (e1 ^ -1 ((⊩)⎻ U));]
+    apply (.= †COM);
     change in ⊢ (? ? ? % ?) with (((⊩)⎻* ∘ (⊩)⎻ ) (((⊩)⎻* ∘ t \sub \c⎻* ∘ (⊩)⎻ ) U));
     apply (.= (lemma_10_3_d ?? (⊩) (t \sub \c⎻* ((⊩)⎻ U))));
-    apply (.= Hcut ^ -1);
+    apply (.= COM ^ -1);
     change in ⊢ (? ? ? % ?) with (t \sub \f⎻* (((⊩)⎻* ∘ (⊩)⎻ ) U));
-    apply (prop11 ?? t \sub \f⎻* );
-    apply (e ^ -1); ]
+    change in e with (U=((⊩)⎻* ∘(⊩ \sub BP1)⎻ ) U);
+    unfold in ⊢ (? ? ? % %); apply (†e^-1);]
 qed.
\ No newline at end of file
diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma b/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma
index 68b9befb8..8847eef31 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma
@@ -1,4 +1,4 @@
-(**************************************************************************)
+ (**************************************************************************)
 (*       ___                                                              *)
 (*      ||M||                                                             *)
 (*      ||A||       A project by Andrea Asperti                           *)
@@ -24,11 +24,6 @@ record basic_topology: Type2 ≝
    compatibility: ∀U,V. (A U >< J V) = (U >< J V)
  }.
 
-lemma hint: OA → objs2 OA.
- intro; apply t;
-qed.
-coercion hint.
-
 record continuous_relation (S,T: basic_topology) : Type2 ≝
  { cont_rel:> arrows2 OA S T;
    (* reduces uses eq1, saturated uses eq!!! *)
@@ -40,24 +35,17 @@ definition continuous_relation_setoid: basic_topology → basic_topology → set
  intros (S T); constructor 1;
   [ apply (continuous_relation S T)
   | constructor 1;
-     [ (*apply (λr,s:continuous_relation S T.∀b. eq1 (oa_P (carrbt S)) (A ? (r⎻ b)) (A ? (s⎻ b)));*)
-       apply (λr,s:continuous_relation S T.r⎻* ∘ (A S) = s⎻* ∘ (A ?));
+     [ alias symbol "eq" = "setoid2 eq".
+       alias symbol "compose" = "category2 composition".
+       apply (λr,s:continuous_relation S T. (r⎻* ) ∘ (A S) = (s⎻* ∘ (A ?)));
      | simplify; intros; apply refl2;
      | simplify; intros; apply sym2; apply e
      | simplify; intros; apply trans2; [2: apply e |3: apply e1; |1: skip]]]
 qed.
 
-definition cont_rel': ∀S,T: basic_topology. continuous_relation_setoid S T → arrows2 ? S T ≝ cont_rel.
-
-coercion cont_rel'.
-
-definition cont_rel'':
- ∀S,T: basic_topology.
-  carr2 (continuous_relation_setoid S T) → ORelation_setoid (carrbt S) (carrbt T).
- intros; apply rule cont_rel; apply c;
-qed.
-
-coercion cont_rel''.
+definition continuous_relation_of_continuous_relation_setoid: 
+  ∀P,Q. continuous_relation_setoid P Q → continuous_relation P Q ≝ λP,Q,c.c.
+coercion continuous_relation_of_continuous_relation_setoid.
 
 (*
 theorem continuous_relation_eq':
@@ -118,11 +106,8 @@ definition continuous_relation_comp:
   | intros;
     apply sym1; 
     change in match ((s ∘ r) U) with (s (r U));
-    (*<BAD>*) unfold FunClass_1_OF_Type_OF_setoid21;
-    unfold objs2_OF_basic_topology1; unfold hint;
-    letin reduced := reduced; clearbody reduced;
-    unfold uncurry_arrows in reduced ⊢ %; (*</BAD>*)
-    apply (.= (reduced : ?)\sup -1);
+    (*<BAD>*) unfold FunClass_1_OF_carr2;
+              apply (.= (reduced : ?)\sup -1);
      [ (*BAD*) change with (eq1 ? (r U) (J ? (r U)));
        (* BAD U *) apply (.= (reduced ??? U ?)); [ assumption | apply refl1 ]
      | apply refl1]
@@ -150,20 +135,15 @@ definition BTop: category2.
        change in e with (a⎻* ∘ A o1 = a'⎻* ∘ A o1);
        change in e1 with (b⎻* ∘ A o2 = b'⎻* ∘ A o2);
        apply (.= e‡#);
-       intro x;
-       change with (b⎻* (a'⎻* (A o1 x)) = b'⎻*(a'⎻* (A o1 x)));
-       alias symbol "trans" = "trans1".
-       alias symbol "prop1" = "prop11".
-       alias symbol "invert" = "setoid1 symmetry".
-       lapply (.= †(saturated o1 o2 a' (A o1 x) : ?));
-        [3: apply (b⎻* ); | 5: apply Hletin; |1,2: skip;
-        |apply ((o_saturation_idempotent ?? (A_is_saturation o1) x)^-1); ]
-       change in e1 with (∀x.b⎻* (A o2 x) = b'⎻* (A o2 x));
+       intro x;          
+       change with (eq1 ? (b⎻* (a'⎻* (A o1 x))) (b'⎻*(a'⎻* (A o1 x)))); 
+       apply (.= †(saturated o1 o2 a' (A o1 x) ?)); [
+         apply ((o_saturation_idempotent ?? (A_is_saturation o1) x)^-1);]
        apply (.= (e1 (a'⎻* (A o1 x))));
-       alias symbol "invert" = "setoid1 symmetry".
-       lapply (†((saturated ?? a' (A o1 x) : ?) ^ -1));
-        [2: apply (b'⎻* ); |4: apply Hletin; | skip;
-        |apply ((o_saturation_idempotent ?? (A_is_saturation o1) x)^-1);]]
+       change with (eq1 ? (b'⎻* (A o2 (a'⎻* (A o1 x)))) (b'⎻*(a'⎻* (A o1 x))));   
+       apply (.= †(saturated o1 o2 a' (A o1 x):?)^-1); [
+         apply ((o_saturation_idempotent ?? (A_is_saturation o1) x)^-1);]
+       apply rule #;]
   | intros; simplify;
     change with (((a34⎻* ∘ a23⎻* ) ∘ a12⎻* ) ∘ A o1 = ((a34⎻* ∘ (a23⎻* ∘ a12⎻* )) ∘ A o1));
     apply rule (#‡ASSOC ^ -1);
@@ -175,8 +155,12 @@ definition BTop: category2.
     apply (#‡(id_neutral_left2 : ?));]
 qed.
 
-definition btop_carr: BTop → Type1 ≝ λo:BTop. carr1 (oa_P (carrbt o)).
-coercion btop_carr.
+definition basic_topology_of_BTop: objs2 BTop → basic_topology ≝ λx.x.
+coercion basic_topology_of_BTop.
+
+definition continuous_relation_setoid_of_arrows2_BTop : 
+  ∀P,Q. arrows2 BTop P Q → continuous_relation_setoid P Q ≝ λP,Q,x.x.
+coercion continuous_relation_setoid_of_arrows2_BTop.
 
 (*
 (*CSC: unused! *)
diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-concrete_spaces.ma b/helm/software/matita/contribs/formal_topology/overlap/o-concrete_spaces.ma
index b00521633..d7e0bf649 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/o-concrete_spaces.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/o-concrete_spaces.ma
@@ -18,7 +18,7 @@ include "o-saturations.ma".
 definition A : ∀b:BP. unary_morphism1 (form b) (form b).
 intros; constructor 1;
  [ apply (λx.□_b (Ext⎽b x));
- | do 2 unfold FunClass_1_OF_Type_OF_setoid21; intros; apply  (†(†e));]
+ | intros; apply  (†(†e));]
 qed.
 
 lemma down_p : ∀S:SET1.∀I:SET.∀u:S⇒S.∀c:arrows2 SET1 I S.∀a:I.∀a':I.a=a'→u (c a)=u (c a').
@@ -42,18 +42,10 @@ record concrete_space : Type2 ≝
 interpretation "o-concrete space downarrow" 'downarrow x = 
   (fun11 __ (downarrow _) x).
 
-definition bp': concrete_space → basic_pair ≝ λc.bp c.
-coercion bp'.
-
-definition bp'': concrete_space → objs2 BP.
- intro; apply (bp' c);
-qed.
-coercion bp''.
-
 definition binary_downarrow : 
   ∀C:concrete_space.binary_morphism1 (form C) (form C) (form C).
 intros; constructor 1;
-[ intros; apply (↓ t ∧ ↓ t1);
+[ intros; apply (↓ c ∧ ↓ c1);
 | intros;
   alias symbol "prop2" = "prop21".
   alias symbol "prop1" = "prop11".
@@ -71,10 +63,6 @@ record convergent_relation_pair (CS1,CS2: concrete_space) : Type2 ≝
            (Ext⎽CS1 (oa_one (form CS1)))
  }.
 
-definition rp' : ∀CS1,CS2. convergent_relation_pair CS1 CS2 → relation_pair CS1 CS2 ≝
- λCS1,CS2,c. rp CS1 CS2 c.
-coercion rp'.
-
 definition convergent_relation_space_setoid: concrete_space → concrete_space → setoid2.
  intros;
  constructor 1;
@@ -87,19 +75,10 @@ definition convergent_relation_space_setoid: concrete_space → concrete_space 
      | intros 3; apply trans2]]
 qed.
 
-
-definition rp'': ∀CS1,CS2.carr2 (convergent_relation_space_setoid CS1 CS2) → arrows2 BP CS1 CS2 ≝
- λCS1,CS2,c.rp ?? c.
-coercion rp''.
-
-
-definition rp''': ∀CS1,CS2.Type_OF_setoid21 (convergent_relation_space_setoid CS1 CS2) → arrows2 BP CS1 CS2 ≝
- λCS1,CS2,c.rp ?? c.
-coercion rp'''.
-
-definition rp'''': ∀CS1,CS2.Type_OF_setoid21 (convergent_relation_space_setoid CS1 CS2) → carr2 (arrows2 BP CS1 CS2) ≝
- λCS1,CS2,c.rp ?? c.
-coercion rp''''.
+definition convergent_relation_space_of_convergent_relation_space_setoid: 
+  ∀CS1,CS2.carr2 (convergent_relation_space_setoid CS1 CS2) → 
+    convergent_relation_pair CS1 CS2  ≝ λP,Q,c.c.
+coercion convergent_relation_space_of_convergent_relation_space_setoid.
 
 definition convergent_relation_space_composition:
  ∀o1,o2,o3: concrete_space.
@@ -110,21 +89,19 @@ definition convergent_relation_space_composition:
  intros; constructor 1;
      [ intros; whd in t t1 ⊢ %;
        constructor 1;
-        [ apply (t1 ∘ t);
+        [ apply (c1 ∘ c);
         | intros;
-          change in ⊢ (? ? ? % ?) with (t\sub\c⎻ (t1\sub\c⎻ (Ext⎽o3 (b↓c))));
-          unfold FunClass_1_OF_Type_OF_setoid21;
+          change in ⊢ (? ? ? % ?) with (c\sub\c⎻ (c1\sub\c⎻ (Ext⎽o3 (b↓c2))));
           alias symbol "trans" = "trans1".
           apply (.= († (respects_converges : ?)));
-          apply (respects_converges ?? t (t1\sub\f⎻ b) (t1\sub\f⎻ c));
-        | change in ⊢ (? ? ? % ?) with (t\sub\c⎻ (t1\sub\c⎻ (Ext⎽o3 (oa_one (form o3)))));
-          unfold FunClass_1_OF_Type_OF_setoid21;
+          apply (respects_converges ?? c (c1\sub\f⎻ b) (c1\sub\f⎻ c2));
+        | change in ⊢ (? ? ? % ?) with (c\sub\c⎻ (c1\sub\c⎻ (Ext⎽o3 (oa_one (form o3)))));
           apply (.= (†(respects_all_covered :?)));
-          apply rule (respects_all_covered ?? t);]
+          apply rule (respects_all_covered ?? c);]
      | intros;
        change with (b ∘ a = b' ∘ a'); 
-       change in e with (rp'' ?? a = rp'' ?? a');
-       change in e1 with (rp'' ?? b = rp ?? b');
+       change in e with (rp ?? a = rp ?? a');
+       change in e1 with (rp ?? b = rp ?? b');
        apply (e‡e1);]
 qed.
 
@@ -147,3 +124,11 @@ definition CSPA: category2.
     change with (id2 ? o2 ∘ a = a);
     apply (id_neutral_left2 : ?);]
 qed.
+
+definition concrete_space_of_CSPA : objs2 CSPA → concrete_space ≝ λx.x.
+coercion concrete_space_of_CSPA.
+
+definition convergent_relation_space_setoid_of_arrows2_CSPA :
+ ∀P,Q. arrows2 CSPA P Q → convergent_relation_space_setoid P Q ≝ λP,Q,x.x.
+coercion convergent_relation_space_setoid_of_arrows2_CSPA.
+
diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-formal_topologies.ma b/helm/software/matita/contribs/formal_topology/overlap/o-formal_topologies.ma
index 4b667546b..e750dcc90 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/o-formal_topologies.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/o-formal_topologies.ma
@@ -15,10 +15,6 @@
 include "o-basic_topologies.ma".
 
 (*
-definition btop_carr': BTop → setoid1 ≝ λo:BTop. carrbt o.
-
-coercion btop_carr'.
-
 definition downarrow: ∀S:BTop. unary_morphism (Ω \sup S) (Ω \sup S).
  intros; constructor 1;
   [ apply (λU:Ω \sup S.{a | ∃b:carrbt S. b ∈ U ∧ a ∈ A ? (singleton ? b)});
@@ -45,9 +41,6 @@ record formal_topology: Type ≝
  }.
 
 (*
-definition bt': formal_topology → basic_topology ≝ λo:formal_topology.bt o.
-
-coercion bt'.
 
 definition ffintersects': ∀S:BTop. binary_morphism1 S S (Ω \sup S).
  intros; constructor 1;
@@ -63,11 +56,6 @@ record formal_map (S,T: formal_topology) : Type ≝
    C2: extS ?? cr T = S
  }.
 
-definition cr': ∀FT1,FT2.formal_map FT1 FT2 → continuous_relation FT1 FT2 ≝
- λFT1,FT2,c. cr FT1 FT2 c.
-
-coercion cr'.
-
 definition formal_map_setoid: formal_topology → formal_topology → setoid1.
  intros (S T); constructor 1;
   [ apply (formal_map S T);
@@ -78,16 +66,6 @@ definition formal_map_setoid: formal_topology → formal_topology → setoid1.
      | simplify; intros 3; apply trans1]]
 qed.
 
-definition cr'': ∀FT1,FT2.formal_map_setoid FT1 FT2 → arrows1 BTop FT1 FT2 ≝
- λFT1,FT2,c.cr ?? c.
-
-coercion cr''.
-
-definition cr''': ∀FT1,FT2.formal_map_setoid FT1 FT2 → arrows1 REL FT1 FT2 ≝
- λFT1,FT2:formal_topology.λc:formal_map_setoid FT1 FT2.cont_rel FT1 FT2 (cr' ?? c).
-
-coercion cr'''.
-
 axiom C1':
  ∀S,T: formal_topology.∀f:formal_map_setoid S T.∀U,V: Ω \sup T.
   extS ?? f (U ↓ V) = extS ?? f U ↓ extS ?? f V.
diff --git a/helm/software/matita/contribs/formal_topology/overlap/relations.ma b/helm/software/matita/contribs/formal_topology/overlap/relations.ma
index 5678b6a89..74a7c7d78 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/relations.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/relations.ma
@@ -21,7 +21,7 @@ notation < "hvbox (x \nbsp \natur term 90 r \nbsp y)"  with precedence 45 for @{
 notation > "hvbox (x \natur term 90 r y)"  with precedence 45 for @{'satisfy $r $x $y}.
 interpretation "relation applied" 'satisfy r x y = (fun21 ___ (satisfy __ r) x y).
 
-definition binary_relation_setoid: SET → SET → SET1.
+definition binary_relation_setoid: SET → SET → setoid1.
  intros (A B);
  constructor 1;
   [ apply (binary_relation A B)
@@ -36,6 +36,10 @@ definition binary_relation_setoid: SET → SET → SET1.
        assumption]]
 qed.
 
+definition binary_relation_of_binary_relation_setoid : 
+  ∀A,B.binary_relation_setoid A B → binary_relation A B ≝ λA,B,c.c.
+coercion binary_relation_of_binary_relation_setoid.
+
 definition composition:
  ∀A,B,C.
   binary_morphism1 (binary_relation_setoid A B) (binary_relation_setoid B C) (binary_relation_setoid A C).
@@ -94,6 +98,15 @@ definition REL: category1.
           first [apply refl | assumption]]]
 qed.
 
+(* 
+definition setoid_of_REL : objs1 REL → setoid ≝ λx.x.
+coercion setoid_of_REL.
+*)
+
+definition binary_relation_setoid_of_arrow1_REL : 
+  ∀P,Q. arrows1 REL P Q → binary_relation_setoid P Q ≝ λP,Q,x.x.
+coercion binary_relation_setoid_of_arrow1_REL.
+
 definition full_subset: ∀s:REL. Ω \sup s.
  apply (λs.{x | True});
  intros; simplify; split; intro; assumption.
@@ -101,15 +114,6 @@ qed.
 
 coercion full_subset.
 
-definition setoid1_of_REL: REL → setoid ≝ λS. S.
-coercion setoid1_of_REL.
-
-lemma Type_OF_setoid1_of_REL: ∀o1:Type_OF_category1 REL. Type_OF_objs1 o1 → Type_OF_setoid1 ?(*(setoid1_of_SET o1)*).
- [ apply rule o1;
- | intros; apply t;]
-qed.
-coercion Type_OF_setoid1_of_REL.
-
 definition comprehension: ∀b:REL. (unary_morphism1 b CPROP) → Ω \sup b.
  apply (λb:REL. λP: b ⇒ CPROP. {x | P x});
  intros; simplify;
diff --git a/helm/software/matita/contribs/formal_topology/overlap/relations_to_o-algebra.ma b/helm/software/matita/contribs/formal_topology/overlap/relations_to_o-algebra.ma
index 856a7e0ae..3317c0e64 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/relations_to_o-algebra.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/relations_to_o-algebra.ma
@@ -52,30 +52,30 @@ definition orelation_of_relation: ∀o1,o2:REL. arrows1 ? o1 o2 → arrows2 OA (
  intros;
  constructor 1;
   [ constructor 1; 
-     [ apply (λU.image ?? t U);
+     [ apply (λU.image ?? c U);
      | intros; apply (#‡e); ]
   | constructor 1;
-     [ apply (λU.minus_star_image ?? t U);
+     [ apply (λU.minus_star_image ?? c U);
      | intros; apply (#‡e); ]
   | constructor 1;
-     [ apply (λU.star_image ?? t U);
+     [ apply (λU.star_image ?? c U);
      | intros; apply (#‡e); ]
   | constructor 1;
-     [ apply (λU.minus_image ?? t U);
+     [ apply (λU.minus_image ?? c U);
      | intros; apply (#‡e); ]
   | intros; split; intro;
-     [ change in f with (∀a. a ∈ image ?? t p → a ∈ q);
-       change with (∀a:o1. a ∈ p → a ∈ star_image ?? t q);
+     [ change in f with (∀a. a ∈ image ?? c p → a ∈ q);
+       change with (∀a:o1. a ∈ p → a ∈ star_image ?? c q);
        intros 4; apply f; exists; [apply a] split; assumption;
-     | change in f with (∀a:o1. a ∈ p → a ∈ star_image ?? t q);
-       change with (∀a. a ∈ image ?? t p → a ∈ q);
+     | change in f with (∀a:o1. a ∈ p → a ∈ star_image ?? c q);
+       change with (∀a. a ∈ image ?? c p → a ∈ q);
        intros; cases f1; cases x; clear f1 x; apply (f ? f3); assumption; ]
   | intros; split; intro;
-     [ change in f with (∀a. a ∈ minus_image ?? t p → a ∈ q);
-       change with (∀a:o2. a ∈ p → a ∈ minus_star_image ?? t q);
+     [ change in f with (∀a. a ∈ minus_image ?? c p → a ∈ q);
+       change with (∀a:o2. a ∈ p → a ∈ minus_star_image ?? c q);
        intros 4; apply f; exists; [apply a] split; assumption;
-     | change in f with (∀a:o2. a ∈ p → a ∈ minus_star_image ?? t q);
-       change with (∀a. a ∈ minus_image ?? t p → a ∈ q);
+     | change in f with (∀a:o2. a ∈ p → a ∈ minus_star_image ?? c q);
+       change with (∀a. a ∈ minus_image ?? c p → a ∈ q);
        intros; cases f1; cases x; clear f1 x; apply (f ? f3); assumption; ]
   | intros; split; intro; cases f; clear f;
      [ cases x; cases x2; clear x x2; exists; [apply w1]
@@ -87,7 +87,7 @@ definition orelation_of_relation: ∀o1,o2:REL. arrows1 ? o1 o2 → arrows2 OA (
 qed.
 
 lemma orelation_of_relation_preserves_equality:
- ∀o1,o2:REL.∀t,t': arrows1 ? o1 o2. eq1 ? t t' → orelation_of_relation ?? t = orelation_of_relation ?? t'.
+ ∀o1,o2:REL.∀t,t': arrows1 ? o1 o2. t = t' → eq2 ? (orelation_of_relation ?? t) (orelation_of_relation ?? t').
  intros; split; unfold orelation_of_relation; simplify; intro; split; intro;
  simplify; whd in o1 o2;
   [ change with (a1 ∈ minus_star_image ?? t a → a1 ∈ minus_star_image ?? t' a);
@@ -108,13 +108,8 @@ lemma orelation_of_relation_preserves_equality:
     apply (. #‡(e‡#)); ]
 qed.
 
-lemma hint: ∀o1,o2:OA. Type_OF_setoid21 (arrows2 ? o1 o2) → carr2 (arrows2 OA o1 o2).
- intros; apply t;
-qed.
-coercion hint.
-
 lemma orelation_of_relation_preserves_identity:
- ∀o1:REL. orelation_of_relation ?? (id1 ? o1) = id2 OA (SUBSETS o1).
+ ∀o1:REL. eq2 ? (orelation_of_relation ?? (id1 ? o1)) (id2 OA (SUBSETS o1)).
  intros; split; intro; split; whd; intro; 
   [ change with ((∀x. x ♮(id1 REL o1) a1→x∈a) → a1 ∈ a); intros;
     apply (f a1); change with (a1 = a1); apply refl1;
@@ -136,13 +131,10 @@ lemma orelation_of_relation_preserves_identity:
   | change with (a1 ∈ a → ∀y.a1 ♮(id1 REL o1) y→y∈a); intros;
     change in f1 with (a1 = y); apply (. f1^-1‡#); apply f;]
 qed.
-(*
-lemma hint2: ∀S,T. carr2 (arrows2 OA S T) → Type_OF_setoid21 (arrows2 OA S T).
- intros; apply c;
-qed.
-coercion hint2.
-*)
+
 (* CSC: ???? forse un uncertain mancato *)
+alias symbol "eq" = "setoid2 eq".
+alias symbol "compose" = "category1 composition".
 lemma orelation_of_relation_preserves_composition:
  ∀o1,o2,o3:REL.∀F: arrows1 ? o1 o2.∀G: arrows1 ? o2 o3.
   orelation_of_relation ?? (G ∘ F) =
@@ -156,10 +148,10 @@ lemma orelation_of_relation_preserves_composition:
     split; [ assumption | exists; [apply w] split; assumption ]
   | cases e; cases x; cases f1; cases x1; clear e x f1 x1; exists; [apply w1 ]
     split; [ exists; [apply w] split; assumption | assumption ]
-  | unfold arrows1_OF_ORelation_setoid; 
+  | unfold arrows1_of_ORelation_setoid; 
     cases e; cases x; cases f; cases x1; clear e x f x1; exists; [ apply w1 ]
     split; [ assumption | exists; [apply w] split; assumption ]
-  | unfold arrows1_OF_ORelation_setoid in e; 
+  | unfold arrows1_of_ORelation_setoid in e; 
     cases e; cases x; cases f1; cases x1; clear e x f1 x1; exists; [apply w1 ]
     split; [ exists; [apply w] split; assumption | assumption ]
   | whd; intros; apply f; exists; [ apply y] split; assumption;
diff --git a/helm/software/matita/contribs/formal_topology/overlap/saturations_to_o-saturations.ma b/helm/software/matita/contribs/formal_topology/overlap/saturations_to_o-saturations.ma
index ce6c6f110..97bfcd6c9 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/saturations_to_o-saturations.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/saturations_to_o-saturations.ma
@@ -20,7 +20,7 @@ include "relations_to_o-algebra.ma".
 
 definition o_operator_of_operator:
  ∀C:REL. (Ω \sup C => Ω \sup C) → (SUBSETS C ⇒ SUBSETS C).
- intros;apply t;
+ intros (C t);apply t;
 qed.
 
 definition is_o_saturation_of_is_saturation:
diff --git a/helm/software/matita/contribs/formal_topology/overlap/subsets.ma b/helm/software/matita/contribs/formal_topology/overlap/subsets.ma
index eaa6954a4..e6d187216 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/subsets.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/subsets.ma
@@ -145,7 +145,7 @@ definition big_intersects:
  ∀A:SET.∀I:SET.unary_morphism2 (setoid1_of_setoid I ⇒ Ω \sup A) (setoid2_of_setoid1 (Ω \sup A)).
  intros; constructor 1;
   [ intro; whd; whd in I;
-    apply ({x | ∀i:I. x ∈ t i});
+    apply ({x | ∀i:I. x ∈ c i});
     simplify; intros; split; intros; [ apply (. (e^-1‡#)); | apply (. e‡#); ]
     apply f;
   | intros; split; intros 2; simplify in f ⊢ %; intro;
@@ -157,7 +157,7 @@ definition big_union:
  ∀A:SET.∀I:SET.unary_morphism2 (setoid1_of_setoid I ⇒ Ω \sup A) (setoid2_of_setoid1 (Ω \sup A)).
  intros; constructor 1;
   [ intro; whd; whd in A; whd in I;
-    apply ({x | ∃i:I. x ∈ t i });
+    apply ({x | ∃i:I. x ∈ c i });
     simplify; intros; split; intros; cases e1; clear e1; exists; [1,3:apply w]
     [ apply (. (e^-1‡#)); | apply (. (e‡#)); ]
     apply x;
-- 
2.39.2