Precedence level of \downarrow changed to match that of the binary one.

diff --git a/helm/software/matita/core_notation.moo b/helm/software/matita/core_notation.moo
index c6f66918d0ba74cc8fb2d384b70ae90fd503c825..025a9899df5ec6058f6af934231d6c6da772d390 100644 (file)
--- a/helm/software/matita/core_notation.moo
+++ b/helm/software/matita/core_notation.moo
@@ -201,7 +201,9 @@ notation "hvbox(a break \circ b)"
   left associative with precedence 55
 for @{ 'compose $a $b }.
 
-notation "hvbox(U break ↓ V)" non associative with precedence 80 for @{ 'fintersects $U $V }.
+notation "↓a" with precedence 55 for @{ 'downarrow $a }.
+
+notation "hvbox(U break ↓ V)" non associative with precedence 55 for @{ 'fintersects $U $V }.
 
 notation "(a \sup b)" left associative with precedence 60 for @{ 'exp $a $b}.
 notation "s \sup (-1)" with precedence 60 for @{ 'invert $s }.

diff --git a/helm/software/matita/library/formal_topology/formal_topologies.ma b/helm/software/matita/library/formal_topology/formal_topologies.ma
index 2acb5642d736b940033b7d6bc3421424879cc748..62b11676a7571bf9b07092fee62e2a36e14326ff 100644 (file)
--- a/helm/software/matita/library/formal_topology/formal_topologies.ma
+++ b/helm/software/matita/library/formal_topology/formal_topologies.ma
@@ -59,7 +59,35 @@ qed.
 interpretation "ffintersects'" 'fintersects U V = (fun1 ___ (ffintersects' _) U V).
 
 record formal_map (S,T: formal_topology) : Type ≝
- { cr:> continuous_relation S T;
+ { cr:> continuous_relation_setoid S T;
    C1: ∀b,c. extS ?? cr (b ↓ c) = (ext ?? cr b) ↓ (ext ?? cr c);
    C2: extS ?? cr T = S
- }.
\ No newline at end of file
+ }.
+
+definition formal_map_setoid: formal_topology → formal_topology → setoid1.
+ intros (S T); constructor 1;
+  [ apply (formal_map S T);
+  | constructor 1;
+     [ apply (λf,f1: formal_map S T.f=f1);
+     | simplify; intros 1; apply refl1
+     | simplify; intros 2; apply sym1
+     | 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 formal_map_composition:
+ ∀o1,o2,o3: formal_topology.
+  binary_morphism1
+   (formal_map_setoid o1 o2)
+   (formal_map_setoid o2 o3)
+   (formal_map_setoid o1 o3).
+ intros; constructor 1;
+  [ intros; whd in c c1; constructor 1;
+     [ apply (comp1 BTop ??? c c1);
+     | intros;
+*)
\ No newline at end of file