Some progress: everything works well now.

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 b13317c67659c3963a9983b9ac3677b54463ad41..4d467fc26fc3853bb0e18f4e09fc9370dbc068ac 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma
@@ -41,16 +41,25 @@ interpretation "concrete relation" 'concr_rel r = (concr_rel __ r).
 interpretation "formal relation" 'form_rel r = (form_rel __ r).
 
 include "o-basic_pairs.ma".
-
+(* Qui, per fare le cose per bene, ci serve la nozione di funtore categorico *)
 definition o_basic_pair_of_basic_pair: cic:/matita/formal_topology/basic_pairs/basic_pair.ind#xpointer(1/1) → basic_pair.
  intro;
  constructor 1;
   [ apply (SUBSETS (concr b));
   | apply (SUBSETS (form b));
-  | constructor 1;
+  | apply (orelation_of_relation ?? (rel b)); ]
+qed.
+
+definition o_relation_pair_of_relation_pair:
+ ∀BP1,BP2.cic:/matita/formal_topology/basic_pairs/relation_pair.ind#xpointer(1/1) BP1 BP2 →
+  relation_pair (o_basic_pair_of_basic_pair BP1) (o_basic_pair_of_basic_pair BP2).
+ intros;
+ constructor 1;
+  [ apply (orelation_of_relation ?? (r \sub \c));
+  | apply (orelation_of_relation ?? (r \sub \f));
+  |
   ]
 qed.
- 
 
 definition relation_pair_equality:
  ∀o1,o2. equivalence_relation1 (relation_pair o1 o2).