From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 16 Jan 2009 00:45:58 +0000 (+0000)
Subject: 1. new coercion(s) from CPropi to CProp
X-Git-Tag: make_still_working~4251
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f4b80554953fa5c452fdc9350d236fb9bcb263dd;p=helm.git

1. new coercion(s) from CPropi to CProp
2. fixed notation for subsetS
3. coercions still have problems: the coercion from objs1 REL is not
   accepted because it is identified with the coercion from objs1 SET
---

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 a7be5cc6c..6140e278e 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/basic_pairs.ma
@@ -193,5 +193,5 @@ definition relS: ∀o: BP. binary_morphism1 (concr o) (Ω \sup (form o)) CPROP.
      | apply (. (#‡e1)‡(e‡#)); assumption]]
 qed.
 
-interpretation "basic pair relation for subsets" 'Vdash2 x y = (fun21 (concr _) __ (relS _) x y).
-interpretation "basic pair relation for subsets (non applied)" 'Vdash = (fun21 ___ (relS _)).
+interpretation "basic pair relation for subsets" 'Vdash2 x y c = (fun21 (concr _) __ (relS c) x y).
+interpretation "basic pair relation for subsets (non applied)" 'Vdash c = (fun21 ___ (relS c)).
diff --git a/helm/software/matita/contribs/formal_topology/overlap/concrete_spaces.ma b/helm/software/matita/contribs/formal_topology/overlap/concrete_spaces.ma
index 07a067e73..46e537864 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/concrete_spaces.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/concrete_spaces.ma
@@ -14,11 +14,12 @@
 
 include "basic_pairs.ma".
 
-(* full_subset e' una coercion che non mette piu' *)
+(* carr1 e' necessario perche' ci sega via la coercion per gli oggetti di REL!
+   (confondendola con la coercion per gli oggetti di SET *)
 record concrete_space : Type1 ≝
  { bp:> BP;
-   converges: ∀a: concr bp.∀U,V: form bp. a ⊩ U → a ⊩ V → a ⊩ (U ↓ V);
-   all_covered: ∀x: concr bp. x ⊩ full_subset (form bp)
+   converges: ∀a: carr1 (concr bp).∀U,V: carr1 (form bp). a ⊩ U → a ⊩ V → a ⊩_bp (U ↓ V);
+   all_covered: ∀x: carr1 (concr bp). x ⊩ form bp
  }.
 
 record convergent_relation_pair (CS1,CS2: concrete_space) : Type1 ≝
diff --git a/helm/software/matita/contribs/formal_topology/overlap/cprop_connectives.ma b/helm/software/matita/contribs/formal_topology/overlap/cprop_connectives.ma
index d6c7084b0..167c33317 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/cprop_connectives.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/cprop_connectives.ma
@@ -31,6 +31,12 @@ coercion Type_of_Type3.
 definition CProp0 : Type1 := Type0.
 definition CProp1 : Type2 := Type1.
 definition CProp2 : Type3 := Type2.
+definition CProp_of_CProp0: CProp0 → CProp ≝ λx.x.
+definition CProp_of_CProp1: CProp1 → CProp ≝ λx.x.
+definition CProp_of_CProp2: CProp2 → CProp ≝ λx.x.
+coercion CProp_of_CProp0.
+coercion CProp_of_CProp1.
+coercion CProp_of_CProp2.
 
 inductive Or (A,B:CProp0) : CProp0 ≝
  | Left : A → Or A B