X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Foverlap%2Fbasic_topologies.ma;h=a48aae41c5c598e23c3420fb90e1eddf5402077c;hb=7c4bb1d1baed259e4301d4cf0ecca7a0e3885d92;hp=013ddb94d5a15db81551249caca71610974733a2;hpb=3cf6181bded05eb63140d1b2ba4f2f5791a73b48;p=helm.git

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 ≝