...

[helm.git] / helm / software / matita / contribs / formal_topology / overlap / basic_topologies.ma

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 013ddb94d5a15db81551249caca71610974733a2..a48aae41c5c598e23c3420fb90e1eddf5402077c 100644 (file)
--- 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 ≝