From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 29 Jun 2010 12:07:37 +0000 (+0000)
Subject: notation made half decent
X-Git-Tag: make_still_working~2892
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7c4bb1d1baed259e4301d4cf0ecca7a0e3885d92;p=helm.git

notation made half decent
---

diff --git a/helm/software/matita/contribs/formal_topology/overlap/apply_functor.ma b/helm/software/matita/contribs/formal_topology/overlap/apply_functor.ma
index 789988194..81cf6d8e2 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/apply_functor.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/apply_functor.ma
@@ -70,7 +70,7 @@ qed.
 
 definition F_comp : 
   ∀C1,C2: CAT2.∀F:arrows3 CAT2 C1 C2.∀o1,o2,o3.
-    binary_morphism2 (Fm ?? F o1 o2) (Fm ?? F o2 o3) (Fm ?? F o1 o3).
+    (Fm ?? F o1 o2) × (Fm ?? F o2 o3) ⇒_2 (Fm ?? F o1 o3).
 intros; constructor 1;
 [ intros (f g); constructor 1;
     [ apply (comp2 C2 ??? (ℳ_2 f) (ℳ_2 g));
@@ -111,7 +111,7 @@ intros; constructor 1;
     lapply (FmP ????? a) as H1; lapply (FmP ????? a') as H2;
     cut (REW ????? (map_arrows2 ?? F ?? (ℳ_1 a)) = 
          REW ????? (map_arrows2 ?? F ?? (ℳ_1 a')));[2:
-      apply (.= H1); apply (.= e); apply H2^-1;]
+      apply (.= H1); apply (.= e); apply (H2^-1);]
     clear H1 H2 e; cases S in a a' Hcut; cases T;
     cases H; cases H1; simplify; intros; assumption;]
 | intro; apply rule #;
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 1ce789ed3..9d4cbbed0 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma
@@ -192,7 +192,7 @@ 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).
+definition BPext: ∀o: BP. (form o) ⇒_1 Ω^(concr o).
  intros; constructor 1;
   [ apply (ext ? ? (rel o));
   | intros;
@@ -200,13 +200,13 @@ definition BPext: ∀o: BP. form o ⇒ Ω \sup (concr o).
     apply refl1]
 qed.
 
-definition BPextS: ∀o: BP. Ω \sup (form o) ⇒ Ω \sup (concr o).
+definition BPextS: ∀o: BP. Ω^(form o) ⇒_1 Ω^(concr o).
  intros; constructor 1;
   [ apply (minus_image ?? (rel o));
   | intros; apply (#‡e); ]
 qed.
 
-definition fintersects: ∀o: BP. binary_morphism1 (form o) (form o) (Ω \sup (form o)).
+definition fintersects: ∀o: BP. (form o) × (form o) ⇒_1 Ω^(form o).
  intros (o); constructor 1;
   [ apply (λa,b: form o.{c | BPext o c ⊆ BPext o a ∩ BPext o b });
     intros; simplify; apply (.= (†e)‡#); apply refl1
@@ -218,9 +218,9 @@ qed.
 interpretation "fintersects" 'fintersects U V = (fun21 ??? (fintersects ?) U V).
 
 definition fintersectsS:
- ∀o:BP. binary_morphism1 (Ω \sup (form o)) (Ω \sup (form o)) (Ω \sup (form o)).
+ ∀o:BP. Ω^(form o) × Ω^(form o) ⇒_1 Ω^(form o).
  intros (o); constructor 1;
-  [ apply (λo: basic_pair.λa,b: Ω \sup (form o).{c | BPext o c ⊆ BPextS o a ∩ BPextS o b });
+  [ apply (λo: basic_pair.λa,b: Ω^(form o).{c | BPext o c ⊆ BPextS o a ∩ BPextS o b });
     intros; simplify; apply (.= (†e)‡#); apply refl1
   | intros; split; simplify; intros;
      [ apply (. #‡((†e^-1)‡(†e1^-1))); assumption
@@ -229,9 +229,9 @@ qed.
 
 interpretation "fintersectsS" 'fintersects U V = (fun21 ??? (fintersectsS ?) U V).
 
-definition relS: ∀o: BP. binary_morphism1 (concr o) (Ω \sup (form o)) CPROP.
+definition relS: ∀o: BP. (concr o) × Ω^(form o) ⇒_1 CPROP.
  intros (o); constructor 1;
-  [ apply (λx:concr o.λS: Ω \sup (form o).∃y:form o.y ∈ S ∧ x ⊩⎽o y);
+  [ apply (λx:concr o.λS: Ω^(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 013ddb94d..a48aae41c 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/basic_topologies.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/basic_topologies.ma
@@ -17,11 +17,11 @@ include "saturations.ma".
 
 record basic_topology: Type1 ≝
  { carrbt:> REL;
-   A: unary_morphism1 (Ω \sup carrbt) (Ω \sup carrbt);
-   J: unary_morphism1 (Ω \sup carrbt) (Ω \sup carrbt);
+   A: Ω^carrbt ⇒_1 Ω^carrbt;
+   J: Ω^carrbt ⇒_1 Ω^carrbt;
    A_is_saturation: is_saturation ? A;
    J_is_reduction: is_reduction ? J;
-   compatibility: ∀U,V. (A U ≬ J V) = (U ≬ J V)
+   compatibility: ∀U,V. (A U ≬ J V) =_1 (U ≬ J V)
  }.
 
 record continuous_relation (S,T: basic_topology) : Type1 ≝
diff --git a/helm/software/matita/contribs/formal_topology/overlap/categories.ma b/helm/software/matita/contribs/formal_topology/overlap/categories.ma
index 30a8159fb..fc2ab9d4d 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/categories.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/categories.ma
@@ -103,7 +103,6 @@ record setoid3: Type4 ≝
    eq3: equivalence_relation3 carr3
  }.
 
-
 interpretation "setoid3 eq" 'eq t x y = (eq_rel3 ? (eq3 t) x y).
 interpretation "setoid2 eq" 'eq t x y = (eq_rel2 ? (eq2 t) x y).
 interpretation "setoid1 eq" 'eq t x y = (eq_rel1 ? (eq1 t) x y).
@@ -414,8 +413,26 @@ 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).
+notation > "A × term 74 B ⇒_1 term 19 C" non associative with precedence 72 for @{'binary_morphism1 $A $B $C}.
+notation > "A × term 74 B ⇒_2 term 19 C" non associative with precedence 72 for @{'binary_morphism2 $A $B $C}.
+notation > "A × term 74 B ⇒_3 term 19 C" non associative with precedence 72 for @{'binary_morphism3 $A $B $C}.
+notation > "B ⇒_1 C" right associative with precedence 72 for @{'arrows1_SET $B $C}.
+notation > "B ⇒_1. C" right associative with precedence 72 for @{'arrows1_SETlow $B $C}.
+notation > "B ⇒_2 C" right associative with precedence 72 for @{'arrows2_SET1 $B $C}.
+notation > "B ⇒_2. C" right associative with precedence 72 for @{'arrows2_SET1low $B $C}.
+
+notation "A × term 74 B ⇒\sub 1 term 19 C" non associative with precedence 72 for @{'binary_morphism1 $A $B $C}.
+notation "A × term 74 B ⇒\sub 2 term 19 C" non associative with precedence 72 for @{'binary_morphism2 $A $B $C}.
+notation "A × term 74 B ⇒\sub 3 term 19 C" non associative with precedence 72 for @{'binary_morphism3 $A $B $C}.
+notation "B ⇒\sub 1 C" right associative with precedence 72 for @{'arrows1_SET $B $C}.
+notation "B ⇒\sub 2 C" right associative with precedence 72 for @{'arrows2_SET1 $B $C}.
+
+interpretation "'binary_morphism1" 'binary_morphism1 A B C = (binary_morphism1 A B C).
+interpretation "'binary_morphism2" 'binary_morphism2 A B C = (binary_morphism2 A B C).
+interpretation "'binary_morphism3" 'binary_morphism3 A B C = (binary_morphism3 A B C).
+interpretation "'arrows1_SET low" 'arrows1_SET A B = (unary_morphism1 A B).
+interpretation "'arrows1_SETlow" 'arrows1_SETlow A B = (unary_morphism1 A B).
+interpretation "'arrows1_SET" 'arrows1_SET A B = (arrows1 SET A B).
 
 definition unary_morphism1_setoid1: setoid1 → setoid1 → setoid1.
  intros;
@@ -450,6 +467,10 @@ definition SET1: objs3 CAT2.
   ]
 qed.
 
+interpretation "'arrows2_SET1 low" 'arrows2_SET1 A B = (unary_morphism2 A B).
+interpretation "'arrows2_SET1low" 'arrows2_SET1low A B = (unary_morphism2 A B).
+interpretation "'arrows2_SET1" 'arrows2_SET1 A B = (arrows2 SET1 A B).
+
 definition setoid1_of_SET1: objs2 SET1 → setoid1 ≝ λx.x.
 coercion setoid1_of_SET1.
 
@@ -462,5 +483,3 @@ coercion objs2_of_category1.
 
 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).
diff --git a/helm/software/matita/contribs/formal_topology/overlap/concrete_spaces_to_o-concrete_spaces.ma b/helm/software/matita/contribs/formal_topology/overlap/concrete_spaces_to_o-concrete_spaces.ma
index 40670ba72..3f2417ec9 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/concrete_spaces_to_o-concrete_spaces.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/concrete_spaces_to_o-concrete_spaces.ma
@@ -16,6 +16,7 @@ include "concrete_spaces.ma".
 include "o-concrete_spaces.ma".
 include "basic_pairs_to_o-basic_pairs.ma".
 
+(*
 (* Qui, per fare le cose per bene, ci serve la nozione di funtore categorico *)
 definition o_concrete_space_of_concrete_space: cic:/matita/formal_topology/concrete_spaces/concrete_space.ind#xpointer(1/1) → concrete_space.
  intro;
@@ -47,3 +48,5 @@ definition o_convergent_relation_pair_of_convergent_relation_pair:
     apply (.= (orelation_of_relation_preserves_equality ???? (commute ?? r)));
     apply (orelation_of_relation_preserves_composition ?? (form BP2)  (rel BP1) ?); ]
 qed.
+
+*)
\ No newline at end of file
diff --git a/helm/software/matita/contribs/formal_topology/overlap/depends b/helm/software/matita/contribs/formal_topology/overlap/depends
index b67a2e7c1..75e9975dc 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/depends
+++ b/helm/software/matita/contribs/formal_topology/overlap/depends
@@ -1,26 +1,26 @@
-basic_pairs_to_basic_topologies.ma basic_pairs.ma basic_pairs_to_o-basic_pairs.ma basic_topologies.ma o-basic_pairs_to_o-basic_topologies.ma
 o-basic_pairs.ma notation.ma o-algebra.ma
+basic_pairs_to_basic_topologies.ma basic_pairs.ma basic_pairs_to_o-basic_pairs.ma basic_topologies.ma o-basic_pairs_to_o-basic_topologies.ma
 o-concrete_spaces.ma o-basic_pairs.ma o-saturations.ma
-basic_pairs.ma notation.ma relations.ma
-saturations.ma relations.ma
 o-saturations.ma o-algebra.ma
-o-algebra.ma categories.ma
-categories.ma cprop_connectives.ma
+saturations.ma relations.ma
+basic_pairs.ma notation.ma relations.ma
 formal_topologies.ma basic_topologies.ma
 o-formal_topologies.ma o-basic_topologies.ma
+o-algebra.ma categories.ma
+categories.ma cprop_connectives.ma
 saturations_to_o-saturations.ma o-saturations.ma relations_to_o-algebra.ma saturations.ma
+subsets.ma categories.ma
 basic_topologies.ma relations.ma saturations.ma
 concrete_spaces.ma basic_pairs.ma
-subsets.ma categories.ma
 relations.ma subsets.ma
 r-o-basic_pairs.ma apply_functor.ma basic_pairs_to_o-basic_pairs.ma o-basic_pairs_to_o-basic_topologies.ma
 concrete_spaces_to_o-concrete_spaces.ma basic_pairs_to_o-basic_pairs.ma concrete_spaces.ma o-concrete_spaces.ma
 o-basic_topologies.ma o-algebra.ma o-saturations.ma
+basic_pairs_to_o-basic_pairs.ma basic_pairs.ma o-basic_pairs.ma relations_to_o-algebra.ma
 notation.ma 
 basic_topologies_to_o-basic_topologies.ma basic_topologies.ma o-basic_topologies.ma relations_to_o-algebra.ma
-basic_pairs_to_o-basic_pairs.ma basic_pairs.ma o-basic_pairs.ma relations_to_o-algebra.ma
-apply_functor.ma categories.ma notation.ma
 cprop_connectives.ma logic/connectives.ma
-o-basic_pairs_to_o-basic_topologies.ma notation.ma o-basic_pairs.ma o-basic_topologies.ma
+apply_functor.ma categories.ma notation.ma
 relations_to_o-algebra.ma o-algebra.ma relations.ma
+o-basic_pairs_to_o-basic_topologies.ma notation.ma o-basic_pairs.ma o-basic_topologies.ma
 logic/connectives.ma 
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 5b29ace1a..24dfb7721 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/formal_topologies.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/formal_topologies.ma
@@ -14,7 +14,7 @@
 
 include "basic_topologies.ma".
 
-
+(*
 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)});
@@ -94,3 +94,4 @@ definition formal_map_composition:
     apply prop1; assumption]
 qed.
 
+*)
\ No newline at end of file
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 0a2e84880..9f1c0fada 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/o-algebra.ma
@@ -53,34 +53,31 @@ interpretation "unary morphism1 comprehension with proof" 'comprehension_by s \e
 (* USARE L'ESISTENZIALE DEBOLE *)
 
 
-notation > "A × B ⇉2,1 C" non associative with precedence 70 for @{binary_morphism1 $A $B $C}.
-notation > "A × B ⇉2,2 C" non associative with precedence 70 for @{binary_morphism2 $A $B $C}.
-notation > "B ⇉1,1 C" non associative with precedence 80 for @{arrows1 SET $B $C}.
-notation > "B ⇉1,2 C" non associative with precedence 80 for @{unary_morphism2 $B $C}.
 notation > "hvbox(a break ≤ b)" non associative with precedence 45 for @{oa_leq $a $b}.
 notation > "a >< b" non associative with precedence 45 for @{oa_overlap $a $b}.
 notation > "⋁ p" non associative with precedence 45 for @{oa_join ? $p}.
 notation > "⋀ p" non associative with precedence 45 for @{oa_meet ? $p}.
+notation > "𝟙" non associative with precedence 90 for @{oa_one}. 
+notation > "𝟘" non associative with precedence 90 for @{oa_zero}. 
 record OAlgebra : Type2 := {
   oa_P :> SET1;
-  oa_leq : oa_P × oa_P ⇉2,1 CPROP;
-  oa_overlap: oa_P × oa_P ⇉2,1 CPROP;
-  oa_meet: ∀I:SET.(I ⇒ oa_P) ⇉1,2 oa_P;
-  oa_join: ∀I:SET.(I ⇒ oa_P) ⇉1,2 oa_P;
+  oa_leq : oa_P × oa_P ⇒_1 CPROP;
+  oa_overlap: oa_P × oa_P ⇒_1 CPROP;
+  oa_meet: ∀I:SET.(I ⇒_2 oa_P) ⇒_2. oa_P;
+  oa_join: ∀I:SET.(I ⇒_2 oa_P) ⇒_2. oa_P;
   oa_one: oa_P;
   oa_zero: oa_P;
   oa_leq_refl: ∀a:oa_P. a ≤ a; 
   oa_leq_antisym: ∀a,b:oa_P.a ≤ b → b ≤ a → a = b;
   oa_leq_trans: ∀a,b,c:oa_P.a ≤ b → b ≤ c → a ≤ c;
   oa_overlap_sym: ∀a,b:oa_P.a >< b → b >< a;
-  oa_meet_inf: ∀I:SET.∀p_i:I ⇒ oa_P.∀p:oa_P.p ≤ (⋀ p_i) = (∀i:I.p ≤ (p_i i));
-  oa_join_sup: ∀I:SET.∀p_i:I ⇒ oa_P.∀p:oa_P.(⋁ p_i) ≤ p = (∀i:I.p_i i ≤ p);
-  oa_zero_bot: ∀p:oa_P.oa_zero ≤ p;
-  oa_one_top: ∀p:oa_P.p ≤ oa_one;
-  oa_overlap_preserves_meet_: 
-      ∀p,q:oa_P.p >< q → 
+  oa_meet_inf: ∀I:SET.∀p_i:I ⇒_2 oa_P.∀p:oa_P.p ≤ (⋀ p_i) = (∀i:I.p ≤ (p_i i));
+  oa_join_sup: ∀I:SET.∀p_i:I ⇒_2 oa_P.∀p:oa_P.(⋁ p_i) ≤ p = (∀i:I.p_i i ≤ p);
+  oa_zero_bot: ∀p:oa_P.𝟘 ≤ p;
+  oa_one_top: ∀p:oa_P.p ≤ 𝟙;
+  oa_overlap_preserves_meet_: ∀p,q:oa_P.p >< q → 
         p >< (⋀ { x ∈ BOOL | match x with [ true ⇒ p | false ⇒ q ] | IF_THEN_ELSE_p oa_P p q });
-  oa_join_split: ∀I:SET.∀p.∀q:I ⇒ oa_P.p >< (⋁ q) = (∃i:I.p >< (q i));
+  oa_join_split: ∀I:SET.∀p.∀q:I ⇒_2 oa_P.p >< (⋁ q) = (∃i:I.p >< (q i));
   (*oa_base : setoid;
   1) enum non e' il nome giusto perche' non e' suriettiva
   2) manca (vedere altro capitolo) la "suriettivita'" come immagine di insiemi di oa_base
@@ -122,7 +119,7 @@ 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 binary_meet : ∀O:OAlgebra. binary_morphism1 O O O.
+definition binary_meet : ∀O:OAlgebra. O × O ⇒_1 O.
 intros; split;
 [ intros (p q); 
   apply (∧ { x ∈ BOOL | match x with [ true ⇒ p | false ⇒ q ] | IF_THEN_ELSE_p ? p q });
@@ -138,7 +135,7 @@ interpretation "o-algebra binary meet" 'and a b =
 
 prefer coercion Type1_OF_OAlgebra.
 
-definition binary_join : ∀O:OAlgebra. binary_morphism1 O O O.
+definition binary_join : ∀O:OAlgebra. O × O ⇒_1 O.
 intros; split;
 [ intros (p q); 
   apply (∨ { x ∈ BOOL | match x with [ true ⇒ p | false ⇒ q ] | IF_THEN_ELSE_p ? p q });
@@ -178,10 +175,10 @@ interpretation "o-algebra join with explicit function" 'oa_join_mk f =
   (fun12 ?? (oa_join ??) (mk_unary_morphism ?? f ?)).
 
 record ORelation (P,Q : OAlgebra) : Type2 ≝ {
-  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_f_ : carr2 (P ⇒_2 Q);
+  or_f_minus_star_ : carr2(P ⇒_2 Q);
+  or_f_star_ : carr2(Q ⇒_2 P);
+  or_f_minus_ : carr2(Q ⇒_2 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,31 +211,31 @@ definition ORelation_of_ORelation_setoid :
 coercion ORelation_of_ORelation_setoid.
 
 definition or_f_minus_star:
- ∀P,Q:OAlgebra.unary_morphism2 (ORelation_setoid P Q) (P ⇒ Q).
+ ∀P,Q:OAlgebra.(ORelation_setoid P Q) ⇒_2 (P ⇒_2 Q).
  intros; constructor 1;
   [ apply or_f_minus_star_;
   | intros; cases e; assumption]
 qed.
 
-definition or_f: ∀P,Q:OAlgebra.unary_morphism2 (ORelation_setoid P Q) (P ⇒ Q).
+definition or_f: ∀P,Q:OAlgebra.(ORelation_setoid P Q) ⇒_2 (P ⇒_2 Q).
  intros; constructor 1;
   [ apply or_f_;
   | intros; cases e; assumption]
 qed.
 
-definition or_f_minus: ∀P,Q:OAlgebra.unary_morphism2 (ORelation_setoid P Q) (Q ⇒ P).
+definition or_f_minus: ∀P,Q:OAlgebra.(ORelation_setoid P Q) ⇒_2 (Q ⇒_2 P).
  intros; constructor 1;
   [ apply or_f_minus_;
   | intros; cases e; assumption]
 qed.
 
-definition or_f_star: ∀P,Q:OAlgebra.unary_morphism2 (ORelation_setoid P Q) (Q ⇒ P).
+definition or_f_star: ∀P,Q:OAlgebra.(ORelation_setoid P Q) ⇒_2 (Q ⇒_2 P).
  intros; constructor 1;
   [ apply or_f_star_;
   | intros; cases e; assumption]
 qed.
 
-lemma arrows1_of_ORelation_setoid : ∀P,Q. ORelation_setoid P Q → (P ⇒ Q). 
+lemma arrows1_of_ORelation_setoid : ∀P,Q. ORelation_setoid P Q → (P ⇒_2 Q). 
 intros; apply (or_f ?? c);
 qed.
 coercion arrows1_of_ORelation_setoid.
@@ -448,4 +445,4 @@ qed.
 
 lemma oa_overlap_sym': ∀o:OA.∀U,V:o. (U >< V) = (V >< U).
  intros; split; intro; apply oa_overlap_sym; assumption.
-qed.
\ No newline at end of file
+qed.
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 245fc4fdb..4c725920b 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
@@ -17,11 +17,11 @@ include "o-saturations.ma".
 
 record Obasic_topology: Type2 ≝
  { Ocarrbt:> OA;
-   oA: Ocarrbt ⇒ Ocarrbt;
-   oJ: Ocarrbt ⇒ Ocarrbt;
+   oA: Ocarrbt ⇒_2 Ocarrbt;
+   oJ: Ocarrbt ⇒_2 Ocarrbt;
    oA_is_saturation: is_o_saturation ? oA;
    oJ_is_reduction: is_o_reduction ? oJ;
-   Ocompatibility: ∀U,V. (oA U >< oJ V) = (U >< oJ V)
+   Ocompatibility: ∀U,V. (oA U >< oJ V) =_1 (U >< oJ V)
  }.
 
 record Ocontinuous_relation (S,T: Obasic_topology) : Type2 ≝
@@ -134,11 +134,11 @@ definition OBTop: category2.
        change in e1 with (b⎻* ∘ oA o2 = b'⎻* ∘ oA o2);
        apply (.= e‡#);
        intro x;          
-       change with (eq1 ? (b⎻* (a'⎻* (oA o1 x))) (b'⎻*(a'⎻* (oA o1 x)))); 
+       change with (b⎻* (a'⎻* (oA o1 x)) =_1 b'⎻*(a'⎻* (oA o1 x))); 
        apply (.= †(Osaturated o1 o2 a' (oA o1 x) ?)); [
          apply ((o_saturation_idempotent ?? (oA_is_saturation o1) x)^-1);]
        apply (.= (e1 (a'⎻* (oA o1 x))));
-       change with (eq1 ? (b'⎻* (oA o2 (a'⎻* (oA o1 x)))) (b'⎻*(a'⎻* (oA o1 x))));   
+       change with (b'⎻* (oA o2 (a'⎻* (oA o1 x))) =_1 b'⎻*(a'⎻* (oA o1 x)));   
        apply (.= †(Osaturated o1 o2 a' (oA o1 x):?)^-1); [
          apply ((o_saturation_idempotent ?? (oA_is_saturation o1) x)^-1);]
        apply rule #;]
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 76a1f4248..e333d2412 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
@@ -21,7 +21,7 @@ intros; constructor 1;
  | 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').
+lemma down_p : ∀S:SET1.∀I:SET.∀u:S ⇒_1 S.∀c:arrows2 SET1 I S.∀a:I.∀a':I.a =_1 a'→u (c a) =_1 u (c a').
 intros; apply (†(†e));
 qed.
 
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 59221c7ba..0e0b02e94 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
@@ -14,6 +14,7 @@
 
 include "o-basic_topologies.ma".
 
+(*
 (*
 definition downarrow: ∀S:BTop. unary_morphism (Ω \sup S) (Ω \sup S).
  intros; constructor 1;
@@ -95,4 +96,4 @@ definition formal_map_composition:
     change with (comp1 BTop ??? a b = comp1 BTop ??? a' b');
     apply prop1; assumption]
 qed.
-
+*)
diff --git a/helm/software/matita/contribs/formal_topology/overlap/r-o-basic_pairs.ma b/helm/software/matita/contribs/formal_topology/overlap/r-o-basic_pairs.ma
index 310ef55eb..b3e69b09c 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/r-o-basic_pairs.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/r-o-basic_pairs.ma
@@ -86,7 +86,7 @@ intro; split; intro; simplify; intro;
   clear Hletin Hletin1; cases Hletin2; whd in x2; 
 qed.
 *)
-lemma curry: ∀A,B,C.binary_morphism1 A B C → A → B ⇒ C.
+lemma curry: ∀A,B,C.(A × B ⇒_1 C) → A → (B ⇒_1 C).
  intros;
  constructor 1;
   [ apply (b c);
@@ -96,8 +96,8 @@ qed.
 notation < "F x" left associative with precedence 60 for @{'map_arrows $F $x}.
 interpretation "map arrows 2" 'map_arrows F x = (fun12 ? ? (map_arrows2 ? ? F ? ?) x).
 
-definition preserve_sup : ∀S,T.∀ f:Ω \sup S ⇒ Ω \sup T. CProp1.
-intros (S T f); apply (∀X:Ω \sup S. (f X) = ?);
+definition preserve_sup : ∀S,T.∀ f:Ω^S ⇒_1 Ω^T. CProp1.
+intros (S T f); apply (∀X:Ω \sup S. (f X) =_1 ?);
 constructor 1; constructor 1;
 [ intro y; alias symbol "singl" = "singleton". alias symbol "and" = "and_morphism".
   apply (∃x:S. x ∈ X ∧ y ∈ f {(x)});
diff --git a/helm/software/matita/contribs/formal_topology/overlap/relations.ma b/helm/software/matita/contribs/formal_topology/overlap/relations.ma
index 662c7d048..eda2cfc6d 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/relations.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/relations.ma
@@ -42,7 +42,7 @@ 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).
+  (binary_relation_setoid A B) × (binary_relation_setoid B C) ⇒_1 (binary_relation_setoid A C).
  intros;
  constructor 1;
   [ intros (R12 R23);
@@ -105,25 +105,24 @@ 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.
+definition full_subset: ∀s:REL. Ω^s.
  apply (λs.{x | True});
  intros; simplify; split; intro; assumption.
 qed.
 
 coercion full_subset.
 
-definition comprehension: ∀b:REL. (unary_morphism1 b CPROP) → Ω \sup b.
- apply (λb:REL. λP: b ⇒ CPROP. {x | P x});
+alias symbol "arrows1_SET" (instance 2) = "'arrows1_SET low".
+definition comprehension: ∀b:REL. (b ⇒_1 CPROP) → Ω^b.
+ apply (λb:REL. λP: b ⇒_1 CPROP. {x | P x});
  intros; simplify;
- alias symbol "trans" = "trans1".
- alias symbol "prop1" = "prop11".
  apply (.= †e); apply refl1.
 qed.
 
 interpretation "subset comprehension" 'comprehension s p =
  (comprehension s (mk_unary_morphism1 ?? p ?)).
 
-definition ext: ∀X,S:REL. binary_morphism1 (arrows1 ? X S) S (Ω \sup X).
+definition ext: ∀X,S:REL. (arrows1 ? X S) × S ⇒_1 (Ω^X).
  apply (λX,S.mk_binary_morphism1 ??? (λr:arrows1 REL X S.λf:S.{x ∈ X | x ♮r f}) ?);
   [ intros; simplify; apply (.= (e‡#)); apply refl1
   | intros; simplify; split; intros; simplify;
@@ -185,7 +184,7 @@ qed.
 *)
 
 (* the same as ⋄ for a basic pair *)
-definition image: ∀U,V:REL. binary_morphism1 (arrows1 ? U V) (Ω \sup U) (Ω \sup V).
+definition image: ∀U,V:REL. (arrows1 ? U V) × Ω^U ⇒_1 Ω^V.
  intros; constructor 1;
   [ apply (λr: arrows1 ? U V.λS: Ω \sup U. {y | ∃x:U. x ♮r y ∧ x ∈ S });
     intros; simplify; split; intro; cases e1; exists [1,3: apply w]
@@ -199,7 +198,7 @@ definition image: ∀U,V:REL. binary_morphism1 (arrows1 ? U V) (Ω \sup U) (Ω \
 qed.
 
 (* the same as □ for a basic pair *)
-definition minus_star_image: ∀U,V:REL. binary_morphism1 (arrows1 ? U V) (Ω \sup U) (Ω \sup V).
+definition minus_star_image: ∀U,V:REL. (arrows1 ? U V) × Ω^U ⇒_1 Ω^V.
  intros; constructor 1;
   [ apply (λr: arrows1 ? U V.λS: Ω \sup U. {y | ∀x:U. x ♮r y → x ∈ S});
     intros; simplify; split; intros; apply f;
@@ -210,7 +209,7 @@ definition minus_star_image: ∀U,V:REL. binary_morphism1 (arrows1 ? U V) (Ω \s
 qed.
 
 (* the same as Rest for a basic pair *)
-definition star_image: ∀U,V:REL. binary_morphism1 (arrows1 ? U V) (Ω \sup V) (Ω \sup U).
+definition star_image: ∀U,V:REL. (arrows1 ? U V) × Ω^V ⇒_1 Ω^U.
  intros; constructor 1;
   [ apply (λr: arrows1 ? U V.λS: Ω \sup V. {x | ∀y:V. x ♮r y → y ∈ S});
     intros; simplify; split; intros; apply f;
@@ -221,7 +220,7 @@ definition star_image: ∀U,V:REL. binary_morphism1 (arrows1 ? U V) (Ω \sup V)
 qed.
 
 (* the same as Ext for a basic pair *)
-definition minus_image: ∀U,V:REL. binary_morphism1 (arrows1 ? U V) (Ω \sup V) (Ω \sup U).
+definition minus_image: ∀U,V:REL. (arrows1 ? U V) × Ω^V ⇒_1 Ω^U.
  intros; constructor 1;
   [ apply (λr: arrows1 ? U V.λS: Ω \sup V. {x | (*∃x:U. x ♮r y ∧ x ∈ S*)
       exT ? (λy:V.x ♮r y ∧ y ∈ S) });
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 842219280..c0cf12090 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
@@ -17,7 +17,7 @@ include "o-algebra.ma".
 
 definition POW': objs1 SET → OAlgebra.
  intro A; constructor 1;
-  [ apply (Ω \sup A);
+  [ apply (Ω^A);
   | apply subseteq;
   | apply overlaps;
   | apply big_intersects;
@@ -48,7 +48,7 @@ definition POW': objs1 SET → OAlgebra.
        assumption]]
 qed.
 
-definition powerset_of_POW': ∀A.oa_P (POW' A) → Ω \sup A ≝ λA,x.x.
+definition powerset_of_POW': ∀A.oa_P (POW' A) → Ω^A ≝ λA,x.x.
 coercion powerset_of_POW'.
 
 definition orelation_of_relation: ∀o1,o2:REL. arrows1 ? o1 o2 → arrows2 OA (POW' o1) (POW' o2).
@@ -90,7 +90,8 @@ 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. t = t' → eq2 ? (orelation_of_relation ?? t) (orelation_of_relation ?? t').
+ ∀o1,o2:REL.∀t,t': arrows1 ? o1 o2. 
+   t = t' → orelation_of_relation ?? t =_2 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);
@@ -112,7 +113,7 @@ lemma orelation_of_relation_preserves_equality:
 qed.
 
 lemma orelation_of_relation_preserves_identity:
- ∀o1:REL. eq2 ? (orelation_of_relation ?? (id1 ? o1)) (id2 OA (POW' o1)).
+ ∀o1:REL. orelation_of_relation ?? (id1 ? o1) =_2 id2 OA (POW' 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;
@@ -140,10 +141,8 @@ 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) =
-   comp2 OA (POW' o1) (POW' o2) (POW' o3)
-    ?? (*(orelation_of_relation ?? F) (orelation_of_relation ?? G)*).
- [ apply (orelation_of_relation ?? F); | apply (orelation_of_relation ?? G); ]
+  orelation_of_relation ?? (G ∘ F) = 
+  comp2 OA ??? (orelation_of_relation ?? F) (orelation_of_relation ?? G).
  intros; split; intro; split; whd; intro; whd in ⊢ (% → %); intros;
   [ whd; intros; apply f; exists; [ apply x] split; assumption; 
   | cases f1; clear f1; cases x1; clear x1; apply (f w); assumption;
@@ -173,7 +172,7 @@ qed.
 
 theorem POW_faithful:
  ∀S,T.∀f,g:arrows2 (category2_of_category1 REL) S T.
-  map_arrows2 ?? POW ?? f = map_arrows2 ?? POW ?? g → f=g.
+  map_arrows2 ?? POW ?? f = map_arrows2 ?? POW ?? g → f = g.
  intros; unfold POW in e; simplify in e; cases e;
  unfold orelation_of_relation in e3; simplify in e3; clear e e1 e2 e4;
  intros 2; cases (e3 {(x)}); 
@@ -183,24 +182,15 @@ theorem POW_faithful:
 qed.
 
 
-lemma currify: ∀A,B,C. binary_morphism1 A B C → A → unary_morphism1 B C.
+lemma currify: ∀A,B,C. (A × B ⇒_1 C) → A → (B ⇒_1 C).
 intros; constructor 1; [ apply (b c); | intros; apply (#‡e);]
 qed.
 
 (*
-alias symbol "singl" = "singleton".
-alias symbol "eq" = "setoid eq".
-lemma in_singleton_to_eq : ∀A:setoid.∀y,x:A.y ∈ {(x)} → (eq1 A) y x.
-intros; apply sym1; apply f;
-qed.  
-
-lemma eq_to_in_singleton : ∀A:setoid.∀y,x:A.eq1 A y x → y ∈ {(x)}.
-intros; apply (e^-1);
-qed.
-*)
-
 interpretation "lifting singl" 'singl x = 
  (fun11 ? (objs2 (POW ?))  (singleton ?) x).
+*)
+
 
 theorem POW_full: ∀S,T.∀f. exT22 ? (λg. map_arrows2 ?? POW S T g = f).
  intros; exists;
@@ -211,17 +201,17 @@ theorem POW_full: ∀S,T.∀f. exT22 ? (λg. map_arrows2 ?? POW S T g = f).
        lapply (#‡prop11 ?? f ?? (†e)); [6: apply Hletin; |*:skip ]]  
      | whd; split; whd; intro; simplify; unfold map_arrows2; simplify; 
         [ split;
-           [ change with (∀a1.(∀x. a1 ∈ f (singleton S x) → x ∈ a) → a1 ∈ f⎻* a);
-           | change with (∀a1.a1 ∈ f⎻* a → (∀x.a1 ∈ f (singleton S x) → x ∈ a)); ]
+           [ change with (∀a1.(∀x. a1 ∈ (f {(x):S}) → x ∈ a) → a1 ∈ f⎻* a);
+           | change with (∀a1.a1 ∈ f⎻* a → (∀x.a1 ∈ f {(x):S} → x ∈ a)); ]
         | split;
-           [ change with (∀a1.(∃y:carr T. y ∈ f (singleton S a1) ∧ y ∈ a) → a1 ∈ f⎻ a);
-           | change with (∀a1.a1 ∈ f⎻ a → (∃y:carr T.y ∈ f (singleton S a1) ∧ y ∈ a)); ]
+           [ change with (∀a1.(∃y:carr T. y ∈ f {(a1):S} ∧ y ∈ a) → a1 ∈ f⎻ a);
+           | change with (∀a1.a1 ∈ f⎻ a → (∃y:carr T.y ∈ f {(a1):S} ∧ y ∈ a)); ]
         | split;
-           [ change with (∀a1.(∃x:carr S. a1 ∈ f (singleton S x) ∧ x ∈ a) → a1 ∈ f a);
-           | change with (∀a1.a1 ∈ f a → (∃x:carr S. a1 ∈ f (singleton S x) ∧ x ∈ a)); ]
+           [ change with (∀a1.(∃x:carr S. a1 ∈ f {(x):S} ∧ x ∈ a) → a1 ∈ f a);
+           | change with (∀a1.a1 ∈. f a → (∃x:carr S. a1 ∈ f {(x):S} ∧ x ∈ a)); ]
         | split;
-           [ change with (∀a1.(∀y. y ∈ f (singleton S a1) → y ∈ a) → a1 ∈ f* a);
-           | change with (∀a1.a1 ∈ f* a → (∀y. y ∈ f (singleton S a1) → y ∈ a)); ]]
+           [ change with (∀a1.(∀y. y ∈ f {(a1):S} → y ∈ a) → a1 ∈ f* a);
+           | change with (∀a1.a1 ∈ f* a → (∀y. y ∈ f {(a1):S} → y ∈ a)); ]]
         [ intros; apply ((. (or_prop2 ?? f (singleton ? a1) a)^-1) ? a1);
            [ intros 2; apply (f1 a2); change in f2 with (a2 ∈ f⎻ (singleton ? a1));
              lapply (. (or_prop3 ?? f (singleton ? a2) (singleton ? a1)));
diff --git a/helm/software/matita/contribs/formal_topology/overlap/saturations.ma b/helm/software/matita/contribs/formal_topology/overlap/saturations.ma
index b78952fdb..cc0db526c 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/saturations.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/saturations.ma
@@ -14,13 +14,11 @@
 
 include "relations.ma".
 
-definition is_saturation: ∀C:REL. unary_morphism1 (Ω \sup C) (Ω \sup C) → CProp1 ≝
- λC:REL.λA:unary_morphism1 (Ω \sup C) (Ω \sup C).
-  ∀U,V. (U ⊆ A V) = (A U ⊆ A V).
+definition is_saturation: ∀C:REL. Ω^C ⇒_1 Ω^C → CProp1 ≝
+ λC:REL.λA:Ω^C ⇒_1 Ω^C. ∀U,V. (U ⊆ A V) =_1 (A U ⊆ A V).
 
-definition is_reduction: ∀C:REL. unary_morphism1 (Ω \sup C) (Ω \sup C) → CProp1 ≝
- λC:REL.λJ:unary_morphism1 (Ω \sup C) (Ω \sup C).
-  ∀U,V. (J U ⊆ V) = (J U ⊆ J V).
+definition is_reduction: ∀C:REL. Ω^C ⇒_1 Ω^C → CProp1 ≝
+ λC:REL.λJ: Ω^C ⇒_1 Ω^C. ∀U,V. (J U ⊆ V) =_1 (J U ⊆ J V).
 
 theorem saturation_expansive: ∀C,A. is_saturation C A → ∀U. U ⊆ A U.
  intros; apply (fi ?? (i ??)); apply subseteq_refl.
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 88a18fda7..0a6700568 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
@@ -18,19 +18,16 @@ include "relations_to_o-algebra.ma".
 
 (* These are only conversions :-) *)
 
-definition o_operator_of_operator:
- ∀C:REL. (Ω \sup C => Ω \sup C) → (POW C ⇒ POW C).
+definition o_operator_of_operator: ∀C:REL. (Ω^C ⇒_1 Ω^C) → ((POW C) ⇒_1 (POW C)).
  intros (C t);apply t;
 qed.
 
-definition is_o_saturation_of_is_saturation:
- ∀C:REL.∀R: unary_morphism1 (Ω \sup C) (Ω \sup C).
+definition is_o_saturation_of_is_saturation: ∀C:REL.∀R: Ω^C ⇒_1 Ω^C.
   is_saturation ? R → is_o_saturation ? (o_operator_of_operator ? R).
  intros; apply i;
 qed.
 
-definition is_o_reduction_of_is_reduction:
- ∀C:REL.∀R: unary_morphism1 (Ω \sup C) (Ω \sup C).
+definition is_o_reduction_of_is_reduction: ∀C:REL.∀R: Ω^C ⇒_1 Ω^C.
   is_reduction ? R → is_o_reduction ? (o_operator_of_operator ? R).
  intros; apply i;
 qed.
\ No newline at end of file
diff --git a/helm/software/matita/contribs/formal_topology/overlap/subsets.ma b/helm/software/matita/contribs/formal_topology/overlap/subsets.ma
index 3c855236b..8eedb5523 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/subsets.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/subsets.ma
@@ -14,10 +14,13 @@
 
 include "categories.ma".
 
-record powerset_carrier (A: objs1 SET) : Type1 ≝ { mem_operator: unary_morphism1 A CPROP }.
+record powerset_carrier (A: objs1 SET) : Type1 ≝ { mem_operator: A ⇒_1 CPROP }.
+interpretation "powerset low" 'powerset A = (powerset_carrier A).
+notation "hvbox(a break ∈. b)" non associative with precedence 45 for @{ 'mem_low $a $b }.
+interpretation "memlow" 'mem_low a S = (mem_operator ? S a).
 
-definition subseteq_operator: ∀A: SET. powerset_carrier A → powerset_carrier A → CProp0 ≝
- λA:objs1 SET.λU,V.∀a:A. mem_operator ? U a → mem_operator ? V a.
+definition subseteq_operator: ∀A: objs1 SET. Ω^A → Ω^A → CProp0 ≝
+ λA:objs1 SET.λU,V.∀a:A. a ∈. U → a ∈. V.
 
 theorem transitive_subseteq_operator: ∀A. transitive2 ? (subseteq_operator A).
  intros 6; intros 2;
@@ -43,7 +46,7 @@ interpretation "powerset" 'powerset A = (powerset_setoid1 A).
 interpretation "subset construction" 'subset \eta.x =
  (mk_powerset_carrier ? (mk_unary_morphism1 ? CPROP x ?)).
 
-definition mem: ∀A. binary_morphism1 A (Ω \sup A) CPROP.
+definition mem: ∀A. A × Ω^A ⇒_1 CPROP.
  intros;
  constructor 1;
   [ apply (λx,S. mem_operator ? S x)
@@ -58,7 +61,7 @@ qed.
 
 interpretation "mem" 'mem a S = (fun21 ??? (mem ?) a S).
 
-definition subseteq: ∀A. binary_morphism1 (Ω \sup A) (Ω \sup A) CPROP.
+definition subseteq: ∀A. Ω^A × Ω^A ⇒_1 CPROP.
  intros;
  constructor 1;
   [ apply (λU,V. subseteq_operator ? U V)
@@ -73,21 +76,18 @@ qed.
 
 interpretation "subseteq" 'subseteq U V = (fun21 ??? (subseteq ?) U V).
 
-
-
-theorem subseteq_refl: ∀A.∀S:Ω \sup A.S ⊆ S.
+theorem subseteq_refl: ∀A.∀S:Ω^A.S ⊆ S.
  intros 4; assumption.
 qed.
 
-theorem subseteq_trans: ∀A.∀S1,S2,S3: Ω \sup A. S1 ⊆ S2 → S2 ⊆ S3 → S1 ⊆ S3.
+theorem subseteq_trans: ∀A.∀S1,S2,S3: Ω^A. S1 ⊆ S2 → S2 ⊆ S3 → S1 ⊆ S3.
  intros; apply transitive_subseteq_operator; [apply S2] assumption.
 qed.
 
-definition overlaps: ∀A. binary_morphism1 (Ω \sup A) (Ω \sup A) CPROP.
+definition overlaps: ∀A. Ω^A × Ω^A ⇒_1 CPROP.
  intros;
  constructor 1;
-  (* Se metto x al posto di ? ottengo una universe inconsistency *)
-  [ apply (λA:objs1 SET.λU,V:Ω \sup A.(exT2 ? (λx:A.?(*x*) ∈ U) (λx:A.?(*x*) ∈ V) : CProp0))
+  [ apply (λA:objs1 SET.λU,V:Ω^A.(exT2 ? (λx:A.x ∈ U) (λx:A.x ∈ V) : CProp0))
   | intros;
     constructor 1; intro; cases e2; exists; [1,4: apply w]
      [ apply (. #‡e^-1); assumption
@@ -98,8 +98,7 @@ qed.
 
 interpretation "overlaps" 'overlaps U V = (fun21 ??? (overlaps ?) U V).
 
-definition intersects:
- ∀A. binary_morphism1 (Ω \sup A) (Ω \sup A) (Ω \sup A).
+definition intersects: ∀A. Ω^A × Ω^A ⇒_1 Ω^A.
  intros;
  constructor 1;
   [ apply rule (λU,V. {x | x ∈ U ∧ x ∈ V });
@@ -112,8 +111,7 @@ qed.
 
 interpretation "intersects" 'intersects U V = (fun21 ??? (intersects ?) U V).
 
-definition union:
- ∀A. binary_morphism1 (Ω \sup A) (Ω \sup A) (Ω \sup A).
+definition union: ∀A. Ω^A × Ω^A ⇒_1 Ω^A.
  intros;
  constructor 1;
   [ apply (λU,V. {x | x ∈ U ∨ x ∈ V });
@@ -127,7 +125,7 @@ qed.
 interpretation "union" 'union U V = (fun21 ??? (union ?) U V).
 
 (* qua non riesco a mettere set *)
-definition singleton: ∀A:setoid. unary_morphism1 A (Ω \sup A).
+definition singleton: ∀A:setoid. A ⇒_1 Ω^A.
  intros; constructor 1;
   [ apply (λa:A.{b | a =_0 b}); unfold setoid1_of_setoid; simplify;
     intros; simplify;
@@ -140,9 +138,9 @@ definition singleton: ∀A:setoid. unary_morphism1 A (Ω \sup A).
 qed.
 
 interpretation "singleton" 'singl a = (fun11 ?? (singleton ?) a).
+notation > "{ term 19 a : S }" with precedence 90 for @{fun11 ?? (singleton $S) $a}.
 
-definition big_intersects:
- ∀A:SET.∀I:SET.unary_morphism2 (setoid1_of_setoid I ⇒ Ω \sup A) (setoid2_of_setoid1 (Ω \sup A)).
+definition big_intersects: ∀A:SET.∀I:SET.(I ⇒_2 Ω^A) ⇒_2 Ω^A.
  intros; constructor 1;
   [ intro; whd; whd in I;
     apply ({x | ∀i:I. x ∈ c i});
@@ -153,8 +151,7 @@ definition big_intersects:
      | apply (. (#‡e i)); apply f]]
 qed.
 
-definition big_union:
- ∀A:SET.∀I:SET.unary_morphism2 (setoid1_of_setoid I ⇒ Ω \sup A) (setoid2_of_setoid1 (Ω \sup A)).
+definition big_union: ∀A:SET.∀I:SET.(I ⇒_2 Ω^A) ⇒_2 Ω^A.
  intros; constructor 1;
   [ intro; whd; whd in A; whd in I;
     apply ({x | ∃i:I. x ∈ c i });